metamatematica
Scienza che ha per oggetto l’analisi formale delle strutture matematiche, e che si può identificare con la logica matematica. Con significato più ristretto la m., o teoria della dimostrazione (Beweistheorie), è la scienza, creata da D. Hilbert intorno al 1919, avente per oggetto intere teorie matematiche e le relative proprietà strutturali. Per l’indirizzo ideato da Hilbert (➔ formalismo), il fine ultimo della m. è di chiarire i fondamenti della matematica, in modo da metterla al riparo dai paradossi; il suo metodo specifico consiste, innanzitutto, nel trasformare una teoria matematica in un sistema assiomatico mediante la piena formalizzazione del suo significato intuitivo e nel dimostrare, poi, le proprietà del sistema formale costruito (in particolare, la sua non contraddittorietà). Il trattamento metamatematico può essere infatti applicato solo a teorie completamente formalizzate (cioè, a sistemi assiomatici contenenti un conveniente calcolo logico, simboli speciali per gli individui, i predicati e le funzioni, oltre agli assiomi non logici propri delle teorie), scelte in modo da riprodurre fedelmente le teorie matematiche oggetto di studio. Perciò si dovrà, tra l’altro, esigere che la teoria formalizzata sia semanticamente completa, cioè che ogni teorema dimostrabile nella teoria matematica originaria trovi il corrispettivo in una proposizione deducibile nella teoria formale. Nella scelta del calcolo logico da includere nella teoria si farà in modo che questo sia non solo sufficientemente potente per esprimere tutte le deduzioni della teoria oggetto di studio, ma contemporaneamente il più debole possibile per evitare complicazioni non indispensabili. Un elemento qualificante della m. hilbertiana è che ogni dimostrazione o costruzione deve essere effettivamente eseguibile in un numero finito di passi, così che non possano sorgere dubbi sulla correttezza delle deduzioni metamatematiche.
Un’importante novità nel metodo metamatematico viene introdotto da K. Gödel, il quale, oltre alla teoria matematica oggetto di studio, formalizza anche la m. stessa. Si può, dunque, dire che con Gödel si chiude la ‘fase ingenua’ della m. e ha inizio il ‘periodo critico’ di una m. formalizzata e cosciente delle proprie interne limitazioni. Lo strumento escogitato da Gödel nel 1931 allo scopo di formalizzare la m. è il procedimento di aritmetizzazione, detto pure di gödelizzazione, grazie al quale le affermazioni metamatematiche, per es. che una certa espressione è dimostrabile, divengono proposizioni aritmetiche, e la m., come la matematica, può essere interamente formalizzata. Se la teoria oggetto di studio è l’aritmetica formalizzata, essendo ormai anche le espressioni metamatematiche divenute aritmetiche, tutta la m. del sistema formale è contenuta in questo stesso sistema, se esso è sufficientemente potente. Così Gödel dimostrò: a) che un tale sistema è sintatticamente incompleto (cioè, esiste una espressione A del sistema per cui né A, né ¬A è deducibile in esso); b) che se un tale sistema è consistente, la sua consistenza non può essere provata all’interno di esso. Dopo che Gödel ebbe dimostrato l’impossibilità di dare una garanzia assoluta della matematica mediante una dimostrazione finitistica della sua non contraddittorietà, furono fornite di questa alcune prove ma con argomentazioni non finitistiche.
Nel 1936 G. Gentzen riuscì a dimostrare la consistenza dell’aritmetica usando un principio d’induzione transfinita. Analoghi risultati sono stati ottenuti da K. Schütte, da P. Lorentzen e altri. Naturalmente questo genere di dimostrazioni non ha l’importanza epistemologica di una dimostrazione di consistenza del tipo progettato da Hilbert. Proprio per questo, anziché alla consistenza assoluta, l’interesse degli studiosi si è rivolto a dimostrazioni di consistenza relativa e d’indipendenza. I due risultati storicamente più importanti sono quelli ottenuti da Gödel e da P. Cohen. Nel 1940 Gödel dimostrò la non contraddittorietà, relativamente agli altri assiomi della teoria degli insiemi, dell’assioma zermeliano della scelta e dell’ipotesi cantoriana del continuo; questa, nel caso più semplice, afferma che non esistono insiemi di potenze comprese tra quella del numerabile e quella del continuo. Nel 1963 Cohen dimostrò anche l’indipendenza dell’ipotesi del continuo dagli altri assiomi.
La m., che era nata come studio di sistemi formali matematici e delle relative questioni di non contraddittorietà e completezza, si è estesa a campi nuovi divenendo una m. in senso ampio. Un esempio importante di tali ampliamenti è dato dalla teoria dei modelli.