Scienza che si occupa dell'analisi formale delle strutture matematiche,
identificabile con la logica matematica. Con significato più ristretto il
termine è stato originariamente introdotto, intorno al 1919, da D.
Hilbert, per indicare il suo programma di ricerca formalista. ║
La m.
di Hilbert o
teoria della dimostrazione: nacque in contrapposizione
sia al logicismo di G. Frege e B. Russel, sia all'intuizionismo di E.J. Brower,
rivendicando, da un lato, l'autonomia dell'attività matematica,
dall'altro il suo carattere finitista. Oggetto della
m. sono intere
teorie matematiche e le loro proprietà strutturali; il suo fine è
quello di chiarire la natura e i limiti della matematica; il suo metodo consiste
nel trasformare una teoria matematica in un sistema assiomatico tramite la
formalizzazione del suo significato intuitivo, e nel dimostrare le
caratteristiche - prima fra tutte la non contraddittorietà - del sistema
così costruito. Infatti, poiché le teorie matematiche formalizzate
non sono altro che enunciati privi di significato, la discriminante per la loro
accettabilità sta nella loro non contraddittorietà. La
realizzazione del progetto hilbertiano comportava una completa formalizzazione
delle teorie matematiche, cioè la creazione di un sistema assiomatico con
un adatto calcolo logico, simboli per individui, predicati e funzioni,
nonché gli assiomi non logici propri delle teorie, in modo da riprodurre
fedelmente le teorie matematiche oggetto di studio. Per far questo era
necessario che la teoria formalizzata fosse semanticamente completa, ovvero che
ogni teorema dimostrabile nella teoria matematica originaria avesse come
corrispettivo una proposizione deducibile nella teoria formale, e che il calcolo
logico fosse sufficientemente potente per esprimere tutte le deduzioni della
teoria. Il fallimento del programma hilbertiano divenne palese dopo la
dimostrazione dei due teoremi di Gödel. ║
La m. di Gödel:
il carattere originale della
m. di K. Gödel sta nella
formalizzazione non solo della teoria matematica oggetto di studio, ma della
m. stessa. Infatti, tramite un particolare meccanismo chiamato
aritmetizzazione o
gödelizzazione, egli riuscì a
trasformare le affermazioni metamatematiche in proposizioni aritmetiche. Se la
teoria in oggetto di studio è l'aritmetica formalizzata, dal momento che
le espressioni metamatematiche sono divenute aritmetiche, tutta la
m. del
sistema formale è contenuta in questo stesso sistema, ammesso che esso
sia sufficientemente potente. Sulla base di questa ipotesi, e facendo ricorso
alla teoria della ricorsività, Gödel dimostrò che un tale
sistema non è sintatticamente completo e che, se esso è coerente,
la sua coerenza non può essere provata all'interno di esso. ║
La
m. dopo Gödel: svanito il progetto di dare una garanzia assoluta della
matematica tramite una dimostrazione finitistica della sua non
contraddittorietà, furono fornite prove di essa su base non finitistica.
Nel 1936, G. Gentzen dimostrò la consistenza dell'aritmetica servendosi
di un principio di induzione transfinita, seguito in questa strada da K.
Schütte e da P. Lorentzen. Altri studiosi hanno preferito rivolgersi a
dimostrazioni di consistenza relativa e di indipendenza; nel 1940 Gödel
dimostrò la non contraddittorietà, relativamente agli altri
teoremi della teoria degli insiemi, dell'assioma zermeliano della scelta e
dell'ipotesi cantoriana del continuo; nel 1963 P. Cohen dimostrò
l'indipendenza dell'ipotesi del continuo dagli altri assiomi. Parallelamente la
m. si è estesa a nuovi campi, passando da studio di sistemi
formali matematici e delle loro questioni di non contraddittorietà e
completezza, a
m. in senso ampio. Ne sono un esempio la teoria dei
modelli e quella della ricorsività generale.