formalismo (matematica)

indirizzo di ricerca sviluppatosi, nell'ambito della logica matematica, in seguito agli studi compiuti sui fondamenti della matematica. Tutta la matematica moderna è formale, in quanto in essa è eliminato, almeno nella sistemazione conclusiva di una teoria, ogni ricorso all'intuizione, al significato concreto degli enti studiati. Il punto di partenza di ogni teoria formalizzata sono alcuni assiomi che definiscono gli enti fondamentali implicitamente, cioè mediante relazioni dette appunto formali, intercorrenti tra di essi. Vi sono poi regole, anche esse formali (da applicare, cioè, come puri schemi) di deduzione di teoremi. Quando la formalizzazione è completa, la verifica della correttezza o meno di una deduzione può essere resa del tutto automatica. Anche la matematica classica è in larga misura formale. Si chiamano proprietà formali delle operazioni, tanto nell'aritmetica classica quanto nell'algebra astratta, alcune relazioni che sono soddisfatte identicamente, cioè per ogni possibile scelta degli elementi sui quali si opera; si ricordano la proprietà associativa e quella commutativa, verificate, per esempio, dalle operazioni di un campo. Il classico successivo ampliamento dei numeri dai naturali ai complessi viene fatto seguendo il principio della conservazione delle proprietà formali nei campi via via più vasti che si costruiscono. In logica matematica, il formalismo cercò di conciliare le esigenze intuizioniste di un'effettiva controllabilità delle teorie matematiche con il tentativo di dare una fondazione logica della matematica, proprio del logicismo. Il programma del formalismo, che prese l'avvio da D. Hilbert e dal suo gruppo negli anni Venti, consiste, in breve, nel formalizzare radicalmente la matematica classica e nel sottoporla poi all'analisi metamatematica, il cui oggetto non è quanto trattato dalla teoria in esame, ma il sistema di formule che compaiono nella teoria formalizzata prescindendo completamente dal loro significato. Si doveva dimostrare la non-contraddittorietà della teoria formalizzata, con metodi finitisti. Sempre negli anni Venti, tutta una serie di risultati ottenuti sembrava confortare tale programma, ma i teoremi di Gödel, agli inizi degli anni Trenta, dimostrarono come non fosse possibile con tali metodi una dimostrazione di non-contraddittorietà per sistemi formali sufficientemente potenti, per esempio tali da esprimere l'aritmetica. Si cercò allora di modificare le condizioni finitiste, nel senso di utilizzare metodi non finitisti, ma accettabili sul piano costruttivista, per vedere se fosse possibile una dimostrazione di non-contraddittorietà delle teorie. Il che, ovviamente, comportava la fine del formalismo originario. Questo nuovo atteggiamento consentì a G. Gentzen di dimostrare la non-contraddittorietà dell'aritmetica utilizzando il principio di induzione limitata. Un risultato analogo fu conseguito da K. Gödel nel 1958. È nello studio di queste estensioni che si è indirizzata la ricerca del formalismo e in questo senso le attuali forme del formalismo si riallacciano alla posizione hilbertiana più in senso metaforico che sostanziale.

B. Curry, Outlines of a Formalist Philosophy of Mathematics, Amsterdam, 1951; A. Robinson, On the Metamathematics of Algebra, Amsterdam, 1951; S. C. Kleene, Introduction of Metamathematics, New York, 1952.