metamatematica

metamatematica

metamatematica o teoria della dimostrazione, termine con cui si indica il programma proposto da D. Hilbert attorno agli anni Venti del secolo scorso al fine di garantire che le usuali procedure dimostrative matematiche siano sufficienti a derivare l’intero corpo della matematica classica, ma non permettano di derivare alcuna contraddizione. Dopo aver costruito dei sistemi formali per varie teorie matematiche, era necessario porsi a un livello teorico superiore, in cui considerare le dimostrazioni della matematica formalizzata come oggetti di un’indagine informale, allo scopo di fornire la prova della coerenza del sistema in esame. Per porsi al riparo dalle critiche rivolte dall’→ intuizionismo alla matematica classica, si richiedeva che i metodi utilizzati nella dimostrazione di coerenza fossero di carattere finitista. La metamatematica si poneva quindi come un’analisi in termini costruttivi delle teorie formali, così da mostrare superfluo il ricorso al transfinito nelle dimostrazioni matematiche. L’irrealizzabilità del programma hilbertiano, almeno nei termini qui esposti, divenne palese in seguito ai teoremi di → Gödel. Da allora, la nozione di teoria della dimostrazione ha subito una notevole trasformazione, divenendo essa stessa oggetto di una trattazione formale e producendo quindi al suo interno metateoremi, in relazione anche alla riformulazione del programma hilbertiano a opera di G. Gentzen (→ deduzione; → sequenti, calcolo dei). Negli anni Sessanta del secolo scorso il logico svedese D. Prawitz ha proseguito il lavoro di Gentzen inquadrando la teoria della dimostrazione nell’ambito della deduzione naturale, che, senza assumere assiomi, stabilisce regole di calcolo più aderenti al procedimento argomentativo “naturale”. La teoria della dimostrazione, sviluppatasi in più direzioni, quali per esempio la teoria della misurazione delle capacità dimostrative delle diverse teorie formali, è al centro del dibattito sui fondamenti della matematica anche per il ruolo che nel frattempo ha assunto la dimostrazione assistita dal computer, la quale non può che avvalersi di sole regole sintattiche.