metamatematica

metamatematica

Parte della logica matematica che ha per oggetto l’analisi formale delle dimostrazioni e delle strutture matematiche. Le sue principali branche sono quindi la teoria della dimostrazione e la teoria dei modelli.

Logica matematica

La m., o teoria della dimostrazione (Beweistheorie), è il settore della logica, creato da Hilbert intorno al 1919, che ha per oggetto intere teorie matematiche e le relative proprietà strutturali. Il fine ultimo della m. è quello di chiarire la natura e indicare i limiti della matematica; 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à sintattiche del sistema formale costruito. Nel corso degli anni la m., sganciandosi dal ruolo di teoria che ha come oggetto principale lo studio dei fondamenti della matematica, ha subito svariate interpretazioni.

La metamatematica di Hilbert

Per salvaguardare la certezza matematica dalla minaccia dei paradossi come quello di Russell nella teoria degli insiemi, Hilbert propose di ridurre la matematica a una collezione di sistemi assiomatici formali, teorizzando la neccessità di dimostrare la coerenza e la completezza di questi sistemi, a cominciare dal più familiare di tutti: l’aritmetica. Per Hilbert vi sono due tipi di teorie assiomatiche: quelle concrete e quelle astratte. Le assiomatizzazioni del primo tipo trasformano le conoscenze empiriche di un certo settore della realtà in teorie scientifiche, come avvenne, per es., a opera di Euclide per la geometria e di Newton per la meccanica. Le teorie astratte, invece, libere da conoscenze empiriche, sono il vero oggetto della matematica. Questa è, infatti, la scienza che costruisce teorie astratte a partire da proposizioni privilegiate (gli assiomi) dalle quali si derivano altre proposizioni formalmente, cioè senza nessun riferimento a significati esterni alla teoria. Mentre la correttezza di una teoria concreta è garantita dallo stesso riferimento di essa ai fatti concreti, le teorie matematiche sono astratte, ossia significative per sé stesse, quindi non possono essere fondate all’esterno; dare una garanzia della correttezza delle teorie matematiche è il problema fondamentale della metamatematica. Per risolverlo non è sufficiente trattare con le tradizionali teorie matematiche che sono definite più o meno accuratamente, e non completamente formalizzate (cosa che, del resto, lo stesso Hilbert si era limitato a fare nel suo primo lavoro metamatematico, le Grundlagen der Geometrie del 1899). Alcune teorie matematiche erano già state perfettamente formalizzate, ma per scopi diversi da quel che si propone Hilbert­; per es., Peano aveva assiomatizzato perfettamente l’a­ritmetica, ma solo per renderla più rigorosa. Il trattamento metamatematico può essere 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, ossia 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 soltanto 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; ciò anche quando si tratti di giustificare una intera teoria matematica. I criteri possibili per dimostrare la consistenza di una teoria sono tre: (1) esibire una realizzazione concreta finita della teoria; (2) mostrare che una realizzazione concreta infinita di essa può essere costruita con mezzi finitistici; (3) dimostrare direttamente che la teoria è non contraddittoria (e per Hilbert questo è il criterio fondamentale). Mediante il primo criterio si può, per es., dimostrare in modo assolutamente ineccepibile che la teoria formale astratta dei gruppi è consistente; di essa è possibile, infatti, esibire una realizzazione concreta finita mediante le relative tabelle di moltiplicazione. Il secondo criterio consente la giustificazione di un sistema assiomatico che formalizza parte della teoria dei numeri essendo costruito da un’infinità potenziale di individui; questo sistema è esso stesso assai utile in metamatematica. Il terzo criterio, in sostanza, consiste nel dimostrare in un numero finito di passi che con i procedimenti dimostrativi contenuti in una certa teoria non è possibile derivare in essa sia l’espressione A sia l’espressione ¬ A. Per far ciò, in base alla legge di Duns Scoto, basterà mostrare che c’è una formula esprimibile nel linguaggio della teoria che non può essere derivata in essa. Prima di tentare la prima prova della consistenza delle teorie matematiche, nelle Grundlagen si dimostra la coerenza del calcolo dei predicati del primo ordine, mediante il terzo criterio. Dopo si passa all’aritmetica. Ecco in sintesi i risultati cui si perviene. Il sistema formale P:

a = a

a = b → [A (a) → A (b)]

a' ≠ 0

a' = b' → a = b

a + 0 = a

a + b' = (a + b)'

{A (0) ⋀∀x [A(x) →A(x')]} → A (a)

è simultaneamente non contraddittorio e semanticamente completo (cioè, tutti gli enunciati validi intuitivamente, formulabili nel suo linguaggio, sono deducibili nel sistema). Tuttavia, mediante P si può formalizzare solo una parte dell’aritmetica; nelle Grundlagen, infatti, si dimostra che in esso non è neppure rappresentabile la funzione prodotto a · b. Invece il sistema formale P′, ottenuto aggiungendo a P il nuovo simbolo · e i due assiomi che definiscono ricorsivamente il prodotto,

a ∙ 0 = 0

a ∙ b' = a ∙ b + a

è sufficiente per la formalizzazione dell’intera teoria elementare dei numeri; però in esso possono essere rappresentati molti enunciati intorno ai numeri naturali finora indecisi ed eventualmente indecidibili con i mezzi elementari a disposizione. In P′ si può, per esempio, esprimere la congettura di Christian Goldbach. Il fatto che P′ è tale da consentire la formulazione di proposizioni di questo genere, mentre conferma la sua potenza espressiva e quindi l’importanza in vista dell’esprimibilità della completa aritmetica, mette pure in luce la difficoltà di estendere a P′ la dimostrazione di completezza semantica che nelle Grundlagen era stata data prima per il sistema P. Il fallimento del programma della m. hilbertiana non dipende però tanto da questa difficoltà quanto dal teorema d’incompletezza di Gödel.

La metamatematica di Gödel

La novità del metodo metamatematico di Gödel sta nel fatto che egli, 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 (➔ Gödel, Kurt), 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. Con queste ipotesi e utilizzando la teoria della ricorsività primitiva, Gödel dimostrò: (1) che un tale sistema è sintatticamente incompleto (cioè, esiste una espressione A del sistema per cui né A, né ¬A è deducibile in esso); (2) che se un tale sistema è consistente, la sua consistenza non può certamente essere provata all’interno di esso.

La metamatematica dopo Gödel

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. Del 1936 è la dimostrazione di Gentzen della consistenza dell’aritmetica usando un principio d’induzione transfinita. Analoghi risultati sono stati ottenuti da Kurt Schütte, da P.W. 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 maggiormente 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 degli altri assiomi. La m., che era nata come studio di sistemi formali matematici e delle relative questioni di non contraddittorietà e completezza, si estende a campi nuovi divenendo una m. in senso ampio. Un esempio importante di tali ampliamenti è dato dalla teoria dei modelli (➔ modelli, teoria dei). Anche la teoria della ricorsività primitiva viene ampliata nella teoria della ricorsività generale ed è applicata nella m.; S.C. Kleene usa il concetto di ricorsività come base di una scala di complessità logica dei predicati nell’insieme dei numeri naturali, la cosiddetta gerarchia di Kleene; R. Péter, Skolem e R.L. Goodstein elaborano i particolari dell’aritmetica e dell’analisi ricorsiva. Il teorema di rappresentazione delle algebre di Boole dimostrato da M. Stone risulta essere equivalente a quello di A. Lindenbaum. Si ricollegano a questi risultati due nuove scienze: la logica algebrica e la metamatematica dell’algebra.

La logica algebrica

La logica matematica, ormai pienamente sviluppata, si ricollega a quell’algebra della logica, che, creata da Boole al primo nascere della logica matematica, aveva dominato fino all’inizio del 20° sec. (➔ logica matematica). Tarski e Lindenbaum sono gli iniziatori di questo indirizzo matematico della logica algebrica, che è lo studio delle strutture algebriche dei sistemi formali. Le cosiddette algebre di Lindenbaum sono algebre che si associano ai diversi tipi di sistemi formali. Ne presentiamo qui due esempi: l’algebra di Lindenbaum L associata alla logica enunciativa e quella, designata con LM, associata a un sistema formale enunciativo con l’insieme M di assiomi non logici. Per costruire l’algebra L, nell’insieme di tutti gli enunciati del calcolo enunciativo {A, B, ...} si definisce una relazione binaria ℛ ponendo A ℛ B se e solo se è dimostrabile A ↔ B. Si verifica facilmente che ℛ è riflessiva, simmetrica e transitiva, quindi è una relazione di equivalenza. Essa induce, allora, nell’insieme di tutti gli enunciati una partizione in classi di equivalenza [A], [B], ... Nell’insieme L di queste classi introduciamo una struttura algebrica definendo l’operazione unaria ′ e le due operazioni binarie ⋃ e ⋂ mediante le definizioni:

[A]' = [¬ A] (complementazione)

[A] ⋃ [B] = [A ⋁ B] (somma logica)

[A] ⋂ [B] = [A ⋀ B] (prodotto logico).

Poniamo inoltre:

[A ⋁¬ A] = 1 (classe di tutte le tautologie)

[A ⋀¬ A] = 0 (classe di tutte le contraddizioni).

Il sistema algebrico (L, ′, ⋂, ⋃, 1, 0) costituisce l’algebra di Lindenbaum del calcolo enunciativo. Si verifica subito che essa è un’algebra di Boole. In modo analogo si costruisce LM definendo nell’insieme di tutti gli enunciati la relazione binaria di equivalenza ℛM ponendo A ℛM B se e solo se da M è derivabile A ↔ B. Indicate le classi di equivalenza indotte da ℛM con [A]M, [B]M,..., nell’insieme LM di queste si definiscono come prima le operazioni ′, ⋃, ⋂ e le classi 1 e 0. L’algebra di Boole (LM, ′, ⋃, ⋂, 1, 0) è l’algebra di Lindenbaum del sistema formale enunciativo con gli assiomi M. Consideriamo l’applicazione di L in LM

f : [A] → [A]_{M ∙}

È facile convincersi che f è un omomorfismo (booleano) suriettivo, quindi LM è l’immagine omomorfa di L. Se indichiamo con I il nucleo di f, ­allora L/I è un’algebra di Boole isomorfa a LM. Possiamo quindi concludere che ogni algebra di Lindenbaum associata a un sistema formale enunciativo con gli assiomi M si può esprimere, a meno di isomorfismi, mediante una coppia ordinata (B, I) di un’algebra di Boole e di un suo ideale. Con ciò i problemi metamatematici del sistema formale considerato sono trasformati in problemi relativi all’algebra di Lindenbaum associata al sistema stesso. È allora possibile utilizzare gli strumenti dell’algebra astratta per risolvere problemi della m., proprio come, dopo Cartesio, i problemi geometrici possono essere risolti con strumenti algebrici. Per es., se (B, I) è l’algebra associata a un sistema formale S, allora la condizione per la consistenza di S è che I sia un ideale proprio di B; inoltre, l’esistenza di modelli di un sistema assiomatico equivale alla rappresentabilità dell’algebra di Lindenbaum a esso associata. Che la logica enunciativa fosse un modello di algebra di Boole era stato subito constatato, ma solo dopo Lindenbaum e Tarski si è sfruttata la possibilità di associare una struttura algebrica a ogni sistema formale. Se si vuole costruire l’algebra di Lindenbaum di un sistema formale predicativo, le operazioni insiemistiche di complementazione, unione e intersezione non sono più sufficienti. Bisogna introdurre altre operazioni. Ciò avviene talvolta usando la teoria degli spazi topologici invece che quella degli insiemi. Anzi, per ottenere strutture algebriche più aderenti ai corrispondenti sistemi logici predicativi, sono stati inventati nuovi tipi di strutture algebriche: le algebre di chiusura e monadiche (Tarski, J.C.C. McKinsey, P.R. Halmos), quelle relazionali (McKinsey, Tarski, B. Jónsson, R.C. Lyndon, L.H. Chin), le algebre cilindriche (Tarski, F.B. Thompson, L. Henkin) e quelle poliadiche (Halmos). In partic., si può ricordare come l’algebra di Lindenbaum dei predicati poliadici fornisca un esempio di algebra poliadica e quella del calcolo dei predicati con identità un esempio di algebra cilindrica.

La metamatematica dell’algebra

Il cosiddetto metodo semantico permette di ricollegare i metodi metamatematici a quelli ordinariamente seguiti nella ricerca matematica. Come anticipazione di questo metodo può essere riconosciuto il metodo di A. Padoa, che già nel 1901 consentì di dimostrare l’indipendenza di un termine da altri in una determinata teoria deduttiva. Il vero fondatore del metodo semantico è, però, Tarski, che nel 1931, con la sua teoria della definizione, si propose di studiare se, dato un insieme I di entità matematiche, esiste in una data teoria T un’espressione Px che sia soddisfatta esattamente dagli individui di I. In caso affermativo si dice che I è definibile in T. Precedentemente, nel 1930, Tarski, analizzando il paradosso del mentitore, aveva dimostrato che «non è possibile, in generale, definire il concetto semantico di verità», proposizione, questa, che presenta un’evidente analogia con il teorema d’incompletezza di Gödel. A proposito di insiemi definibili, vanno segnalate le ricerche di A. Mostowski, che si ricollegano al concetto di computabilità e a quello di ordine costruttivo. Tarski aveva da tempo previsto pure che alcune idee della m. potevano essere usate nella dimostrazione degli stessi teoremi matematici; ciò fu effettivamente fatto all’inizio degli anni Cinquanta da A. Robinson e Henkin. Questa nuova scienza è stata chiamata m. dell’algebra. Notevoli contributi alla m. dei sistemi algebrici sono stati dati anche in connessione con la teoria dei modelli. Teoria dei modelli e m. dell’algebra si completano vicendevolmente.

Intuizionismo

Per questa corrente di studi metamatematici che è stata professata da Brouwer e dalla sua scuola di Amsterdam, anche prima della m. hilbertiana (➔ intuizionismo).