sistema formale

sistema formale

sistema formale apparato simbolico mediante il quale è possibile rappresentare formalmente i procedimenti logico-deduttivi delle dimostrazioni matematiche. Esempi di sistemi formali sono i calcoli logici quali il calcolo degli → enunciati o il calcolo dei → predicati. I sistemi formali hanno lo scopo di formalizzare le teorie matematiche: si pensi al sistema di assiomi di → Peano per l’aritmetica o al sistema di assiomi di Zermelo-Fraenkel per la teoria degli insiemi (→ Zermelo-Fraenkel, teoria di). La nozione di sistema formale, come attualmente si intende, è frutto degli studi di D. Hilbert e della sua scuola.

Un sistema formale si compone di un apparato linguistico e di un apparato deduttivo. L’apparato linguistico (formato da → alfabeto, → termini e → formule ben formate) determina il linguaggio del sistema formale. Tale linguaggio è costruito fissando un insieme di simboli primitivi (alfabeto) e assegnando una serie di regole che individuano, nell’insieme di tutte le sequenze finite di simboli primitivi, determinate sequenze dette termini e formule che costituiscono i “nomi” degli oggetti di cui parla la teoria formalizzata nel sistema e le sue “proposizioni”. L’apparato deduttivo (costituito da → assiomi e regole di → inferenza) ha lo scopo di definire il concetto di dimostrazione assegnando alcune formule di base (gli assiomi) dalle quali possono essere dedotti tutti i teoremi della teoria mediante l’applicazione delle regole di inferenza.

Le dimostrazioni, in un sistema formale, sono sequenze finite di formule: quelle ottenute a partire dagli assiomi per reiterata applicazione delle regole di deduzione. L’ultima formula di una dimostrazione è detta teorema. In generale è caratteristica fondamentale di tutte queste regole la loro effettività: esse permettono di decidere meccanicamente, in un numero finito di passi, se un dato segno è un simbolo primitivo, se una qualunque sequenza di simboli primitivi è un termine o una formula, se una qualunque formula data è un assioma, se una data sequenza di formule è una dimostrazione. (Va osservato che dalla effettività della nozione di dimostrazione non discende quella della nozione di teorema: le regole, infatti, non forniscono in generale un metodo per accertare, data una qualunque formula, se questa possiede una dimostrazione e, in caso affermativo, come la si possa costruire). Il senso ultimo della sostituzione, a teorie intuitive, di corrispondenti sistemi formali è che, in tal modo, le teorie diventano totalmente oggettivate e si rende così possibile una rigorosa scienza delle teorie, o metateoria. Tutte le teorie perfettamente assiomatizzate ammettono descrizioni in termini di sistemi formali. Esistono anche sistemi formali, più spesso detti sistemi semiformali, con caratteristiche diverse da quelle descritte; taluni, per esempio, possiedono un insieme di simboli primitivi molto astratto, per esempio non numerabile o indecidibile, altri ammettono formule o dimostrazioni anche di lunghezza infinita. Per questi, come per gli altri, vale sempre il fatto che sono oggetti di feconda ricerca metateorica. Data una formula del linguaggio di un sistema formale, si dice che essa è valida quando è soddisfatta da ogni possibile → interpretazione o modello della teoria.

Fra i più importanti problemi che concernono i sistemi formali si ricordano: la → completezza logica, sia semantica (se tutte le formule valide sono teoremi), sia sintattica (se ogni formula del sistema è o dimostrabile o refutabile); la → categoricità (se tutti i modelli del sistema formale sono fra loro isomorfi); la → coerenza (se non sono dimostrabili una formula e la sua negazione). Ulteriori problemi riguardanti i sistemi formali sono l’→ indipendenza e la → decidibilità: la prima vale quando nessuno degli assiomi è dimostrabile a partire dagli altri, la seconda quando esiste un metodo effettivo per determinare se una qualunque formula è o no un teorema. È possibile mostrare che ampie e significative classi di sistemi formali sono semanticamente complete. Per quella fondamentale teoria che è la teoria dei numeri, si dimostra invece che i più importanti sistemi formali corrispondenti, pur semanticamente completi, sono incompleti sintatticamente, indecidibili e non categorici.