La logica nel Novecento

Il contributo è tratto da Storia della civiltà europea a cura di Umberto Eco, edizione in 75 ebook

All’inizio del Novecento la logica si sviluppa sotto l’egida della problematica circa fondamenti della matematica per poi acquisire, a partire dagli anni Trenta, una propria specificità e autonomia concettuale. Fondamentali al riguardo sono il teorema di completezza per la logica del primo ordine, la chiarificazione di decisive nozioni semantiche (modello, conseguenza logica, ecc.), l’introduzione di calcoli per la deduzione che possiedono una natura algoritmica. 

Rapporto tra logica e matematica

Nella prima metà del Novecento l’indagine sui fondamenti della matematica, ossia sulle condizioni – che poi si scoprono interne alla mente umana – che rendono possibile l’applicazione del procedere simbolico (e quindi matematico) ai fatti del mondo esterno, ha comprensibilmente un effetto catalitico sullo sviluppo della logica che, riconosciuta come la teoria matematica del pensiero, diventa la disciplina che oggi conosciamo: concettualmente filosofica e tecnicamente matematica.

Gottlob Frege è considerato il padre della logica moderna: a lui si deve la formalizzazione della quantificazione, ossia l’invenzione di simboli od operatori – i quantificatori, appunto – attraverso i quali è possibile stabilire l’ambito, l’estensione di un termine di una proposizione logica, e la codificazione di un sistema di regole che permette di ottenere, componendo tali simboli, tutte le possibili espressioni. Frege, in altre parole, costruisce “un linguaggio in formule del pensiero puro” attraverso il quale vuole escludere ogni forma di intuizione o di appoggio empirico e psicologico del pensiero (matematico), presentandolo come deduzione logica da concetti logicamente definiti e da assunzioni vere. Ne deriva che la logica di Frege è una disciplina totalizzante: non esistono punti di vista a essa esterni e superiori, non è possibile né l’isolamento del linguaggio della logica del primo ordine da quello della logica di ordine superiore né, soprattutto, formulare questioni concernenti il sistema deduttivo stesso come, per esempio, la questione della sua coerenza (il sistema di riferimento riesce a evitare di farci dimostrare una cosa e il suo contrario?) e la questione della sua completezza (il sistema riesce a dimostrare tutte e solo le verità logiche?).

Questa immagine monolitica della logica filtra sostanzialmente immutata attraverso i tre volumi dei Principia Mathematica di Bertrand Russell e Alfred North Whitehead, i quali tentano una ricostruzione, da un punto di vista logicista, dell’intero edificio della matematica classica, ritenendo che tutte le proposizioni delle matematiche pure (aritmetica e analisi, in particolare) possano essere enunciate attraverso il solo vocabolario e la sola sintassi della logica, che diventa la disciplina matematica per eccellenza.

Completamente innovativo è, invece, il punto di vista di David Hilbert e della sua scuola – nata a partire dagli anni Venti del Novecento – che dà alla matematica, e alla geometria in particolar modo, una base assiomatica: egli considera veri gli assiomi in quanto arbitrariamente stabiliti, e conseguentemente veri tutti gli enti definiti per mezzo di quegli assiomi.

Sulla base di questa premessa, si viene costruendo il cosiddetto metodo assiomatico: nel corso di quegli anni si lavora sugli assiomi, se ne cancellano alcuni e se ne creano altri in modo tale da selezionare solo tutto ciò che è necessario ma non sovrabbondante per la deduzione dei teoremi voluti. Sebbene la ricerca di Hilbert non sia svolta con strumenti formali, ne vien fuori un sistema formale, cioè un sistema per generare teoremi, usando un insieme prefissato di assiomi e di regole d’inferenza, di modo che, auspicabilmente, si dovrebbe essere in grado di verificare attraverso una procedura meccanica se una data formula è dimostrabile oppure no all’interno del sistema stesso. In conclusione le dimostrazioni possono essere trattate come oggetti matematici (finiti) e studiati matematicamente.

Nel 1928 Hilbert e il suo allievo Wilhelm Ackermann, pubblicano il primo testo di logica che può leggersi come un moderno manuale: i Grundzüge der theoretischen Logik (Lineamenti di logica teoretica). In quest’opera gli studiosi, dopo aver separato la logica proporzionale dalla logica del primo ordine, avviano l’indagine metateorica del sistema formale, sollevando due fondamentali questioni: la completezza e la decidibilità.

La nascita della teoria dei modelli

Nei primi anni del Novecento tanto le riflessioni dei logicisti, quanto quelle dei formalisti trovano un comune riferimento nelle concezioni intuizioniste enunciate da Luitzen Brouwer, secondo cui la validità della matematica classica è dimostrabile solo riducendola a un sistema finitistico valido a priori; von Neumann, in particolare, mette in evidenza una sorta di collegamento tra i risultati ottenuti dai diversi indirizzi del tempo, attribuendo soprattutto agli intuizionisti il merito di aver saputo trasformare le vaghe questioni di carattere filosofico-epistemologico dei fondamenti della matematica in tre problemi “precisi”: la formulazione dei difetti della matematica classica (a opera di Brouwer), la descrizione dei suoi metodi (per merito di Russell) e la ricerca matematico-combinatoria di questi metodi e delle loro relazioni (di Hilbert). Con von Neumann si apre allora una ipotesi di conferma della validità della matematica che è legittimabile non attraverso l’indagine dei suoi enunciati, bensì dei suoi metodi: va determinato a quali combinazioni (finite) di simboli primitivi conducono i suoi metodi combinatori, ovvero le dimostrazioni.

Gli anni Trenta si aprono con l’elaborazione del teorema di completezza di Gödel che sembra confermare l’ipotesi possibilista di von Neumann. Tuttavia, negli stessi anni, si va profilando un altro filone logico che risale a Schröder ed è caratterizzato da un approccio semantico, interpretativo, alle teorie formali e che contrasta il filone logicista e formalista che preferisce, invece, un approccio di natura sintattica. In altre parole gli studiosi che fanno capo a questo nuovo filone indagano le teorie definite attraverso il linguaggio predicativo di primo ordine non in termini di “assioma”, “dimostrazione”, “non contraddittorietà” ecc., cioè non sotto l’aspetto sintattico, bensì in termini di “validità”, “verità”, “soddisfacibilità” ecc., cioè dal punto di vista semantico. Questo approccio ha un carattere molto più intuitivo: ogni teoria espressa nel linguaggio del primo ordine può essere interpretata in domini diversi, cioè si può selezionare un insieme qualsiasi come universo di riferimento all’interno del quale collegare – cioè interpretare – ciascun segno linguistico della teoria con elementi appartenenti al dominio stesso di riferimento. Si potrà facilmente intuire che una data formula è vera o falsa se, all’interno del dominio scelto, la sua interpretazione darà origine a proposizioni vere o false. Di conseguenza una formula (o una teoria, ossia un insieme di formule) si dirà soddisfacibile se esiste un dominio all’interno del quale, tramite opportuna interpretazione, la formula (o l’insieme di formule date dagli assiomi della teoria) darà origine a una proposizione vera; sarà non soddisfacibile in caso contrario. Andando oltre, possiamo aggiungere che se la teoria è soddisfacibile in un dominio si dice che ammette un modello costituito dal dominio stesso con tutte le relazioni e le operazioni possibili in esso. Nasce quindi la cosiddetta teoria dei modelli che è alla base di un altro teorema di enorme portata. Si tratta del cosiddetto teorema di Löwenheim-Skolem, anticipato da Leopold Löwenheim (1878-1957) nel 1915 nella memoria Über Möglichkeiten im Relativkalkül (Sulle possibilità nel calcolo dei relativi), e poi generalizzato da Thoralf Skolem (1887-1963) nel 1920 e nel 1922; esso afferma che se un insieme di enunciati del primo ordine è soddisfacibile (e quindi ha un modello), allora è soddisfacibile in un dominio infinito numerabile. Il teorema verte sulla ricerca di una base per le formule nella classe di modelli e conclude che tale base è data dalle interpretazioni numerabili, dal momento che se una formula è soddisfatta in tutte le sue interpretazioni numerabili, allora è logicamente valida. Già Löwenheim si era reso conto che le interpretazioni finite non sono sufficienti a valutare la validità di una formula: era per questo passato a considerare un dominio infinito numerabile (come l’insieme dei Numeri Naturali).

Già nel 1904 il geometra Oswald Veblen (1880-1960) aveva sottolineato il ruolo della nozione di categoricità (classi di modelli) nell’assiomatizzazione di una teoria: un sistema di assiomi è categorico se tutti i suoi modelli sono isomorfi fra loro. Così, il teorema di Löwenheim-Skolem implica che nessun insieme di enunciati del primo ordine può essere una descrizione categorica di una struttura infinita.

Continuando sulla strada del finitismo già introdotto da Hilbert, Skolem inoltre presenta un nuovo possibile modo di sviluppare l’aritmetica di straordinaria importanza per l’odierna teoria dei modelli: egli escogita una tecnica per “eliminare” alla base la fonte stessa dei paradossi generati nei precedenti ragionamenti logici, ovverossia i quantificatori illimitati. Egli infatti ritiene di poter rendere l’aritmetica una scienza rigorosa senza l’utilizzo degli operatori “sempre” e “qualche volta”, ricorrendo all’introduzione di queste variabili logiche apparenti solo in domini finiti e utilizzando come base il metodo ricorsivo di pensare.

Un ulteriore merito di Skolem sta nell’aver applicato il teorema precedente alla teoria degli insiemi, scoprendo il cosiddetto paradosso di Skolem: se il sistema assiomatico di Zermelo (la teoria degli insiemi) è coerente, allora è soddisfacibile in un dominio numerabile. Il paradosso sta nel fatto che gli assiomi della teoria degli insiemi affermano l’esistenza di insiemi infiniti più che numerabili, ma poiché questi stessi assiomi possono essere espressi come enunciati del primo ordine, essi sono soddisfacibili in un modello numerabile.

Per la stessa aritmetica Skolem costruirà nel 1934 un “modello non standard”, cioè non isomorfo alla struttura dei naturali, poiché contiene “altri” oggetti, pur soddisfacendone gli assiomi dell’aritmetica. Del resto, l’esistenza di modelli non standard dell’aritmetica è una diretta conseguenza del primo teorema di incompletezza di Gödel.

Il lavoro di Skolem ha ispirato quello di Abraham Robinson (1918-1974) alla fine degli anni Cinquanta, il quale scopre modelli non standard della teoria dei Reali, realizzando così il progetto leibniziano di formulare una teoria matematicamente coerente degli infinitesimali.

La completezza semantica della logica del primo ordine

Un teorema di completezza può essere visto sotto la forma di una giustificazione delle regole d’inferenza di una teoria logica o, più in generale, come l’organizzazione di uno spazio logico: le regole sono sufficientemente “forti” da dimostrare tutte e solo le formule valide della teoria. Pertanto, un teorema di completezza assicura una corrispondenza tra la nozione di verità, che ha una natura infinitaria e statica, e la nozione di dimostrabilità, che ha invece una natura finitaria ma dinamica. La completezza semantica della logica proposizionale era stata dimostrata nel 1918 da Paul Bernays (1888-1977) e indipendentemente da Emil Post (1897-1954) nel 1921. Nel 1929 nella sua dissertazione dottorale Kurt Gödel dimostra la completezza del calcolo dei predicati del primo ordine. Nel 1949 la dimostrazione di questo risultato è perfezionata e semplificata da Leon Henkin, quando ormai le acquisizioni semantiche di Tarski sono moneta corrente. La nuova dimostrazione, molto elegante, ha un carattere non costruttivo, perché sfrutta il fatto che la coerenza sintattica è la controparte semantica della proprietà di un modello.

Dal teorema di completezza si ottiene come corollario il teorema di compattezza: se T è un insieme di enunciati della logica del primo ordine, e ogni sottoinsieme finito di T ha un modello, allora T ha un modello. Nel 1969 il logico Per Lindström ottiene un notevole risultato che permette di assegnare alla logica del primo ordine un posto unico tra tutti i sistemi logici: nessun sistema logico più espressivo di quello del primo ordine può godere sia della completezza (o compatezza) che del teorema di Löwenheim-Skolem.

La semantica tarskiana

Nella dimostrazione del teorema di completezza per la logica del primo ordine, Gödel aveva trattato la nozione di verità in modo intuitivo, facendo a meno della definizione di validità. Negli anni Trenta, il logico polacco Alfred Tarski (1901-1983) a partire dal saggio Der Wahreitsbegriff in den formalisierten Sprachen (Il concetto di verità nei linguaggi formalizzati) – scritto nel 1933 e pubblicato nel 1935 – completa la matematizzazione della logica fornendo una definizione di verità che pone la basi della semantica dei linguaggi formalizzati. Per Tarski ogni teoria adeguata della verità deve implicare tutte le istanze dello schema chiamato “convenzione V”: [E] è vero se e soltanto se E, dove [E] è un enunciato del linguaggio oggetto ed E la sua traduzione nel metalinguaggio, cioè in quel linguaggio che ha per oggetto il linguaggio in cui è espresso l’enunciato stesso (un esemplificazione della convenzione V può essere: l’enunciato “la calcite è un minerale” è vero se e solo se la calcite è un minerale). La convenzione V è solo una precondizione della definizione di verità: si limita cioè a esprimere l’idea, già aristotelica, che un enunciato è vero semplicemente quando rispecchia uno stato di cose. La definizione tarskiana di verità gravita intorno alla relazione di soddisfacimento, a sua volta cruciale per definire il concetto di modello. Un’interpretazione è una funzione v che associa un valore di verità a ogni enunciato ben formato E di un sistema formale; un’interpretazione v è un modello per E, se v(E) = vero, ossia quando E è soddisfatto nell’interpretazione. Tarski è così in grado di precisare la nozione di conseguenza logica che era stata identificata da Bernhard Bolzano (1781-1848) circa un secolo prima: un enunciato è valido se ogni interpretazione v è un suo modello; un enunciato E è una conseguenza logica di un insieme di enunciati I se e solo se ogni modello di I è anche un modello dell’enunciato E. In breve, la conseguenza logica preserva la verità (non può verificarsi che le premesse siano vere e la conclusione falsa).

L’indecidibilità della logica del primo ordine

L’altra importante questione posta da Hilbert e Ackermann nei Grundzüge può essere formulata in questo modo: data un’arbitraria formula F della logica del primo ordine, esiste un algoritmo che permette di decidere se F è derivabile? È il cosiddetto Entscheidungsproblem, cioè il problema della decisione. “La sua risoluzione ”– scrive il francese Jacques Herbrand (1908-1931) un paio di anni più tardi – “permetterebbe alla logica matematica di svolgere rispetto alla matematica classica lo stesso ruolo della geometria analitica rispetto alla geometria”. Nel 1915 Löwenheim aveva dimostrato la decidibilità del frammento della logica del primo ordine con soli predicati monadici, cioè con quei giudizi (predicati) che si riferiscono a un solo oggetto (argomento).

Ma nel 1936 il logico Alonzo Church (1903-1995) dimostra l’impossibilità di soluzione all’Entscheidungsproblem, un risultato limitativo che segue di qualche anno la dimostrazione dell’incompletezza sintattica di ogni sistema formale sufficientemente espressivo da ambire a rappresentare l’aritmetica già affrontata da Gödel. In virtù del teorema di completezza, l’indecidibilità del problema della derivabilità può anche essere vista come l’indecidibilità del problema della validità. Nel 1937 Alan M. Turing (1912-1954) ottiene, indipendentemente, il medesimo risultato ma attraverso un differente metodo, più diretto e fecondo di quello di Church: l’indecidibilità dell’Entscheidungsproblem viene ridotta a un problema che non si può risolvere attraverso un modello astratto di macchina che in seguito fu chiamata “macchina di Turing” e che si rivelerà lo strumento più adeguato per caratterizzare la complessità temporale e spaziale degli algoritmi. Molto significativamente, nel 1947 Post mostra che l’indecidibilità ha una controparte puramente “algebrica”, dimostrando che il problema della parola per i semigruppi è insolubile – risultato esteso ai gruppi nel 1952 da Petr Novikov (1901-1975). Nel 1958 Andrej Markov (1903-1979) dimostra che esiste un’indecidibilità ancora più culturalmente distante dalla logica: il problema dell’omeomorfismo di varietà topologiche di dimensione 4 è indecidibile.

La teoria della dimostrazione

Nel senso più ampio la teoria della dimostrazione studia le proprietà dei sistemi deduttivi usando metodi formali. I primi sistemi che formalizzano il ragionamento deduttivo sono di tipo assiomatico: essi presentano un insieme di assiomi che esprimono le proprietà delle nozioni logiche e, a partire da questo insieme, si ottengono teoremi applicando la regola del modus ponens, cioè quel processo, fondamentale nel nostro ragionare, che consente di concatenare fra loro delle proposizioni, traendone delle conclusioni. La prima formulazione del calcolo proposizionale come sistema formale si deve a Frege nei suoi Begriffschrifts (Ideografia) del 1879 e fu ripresa da Russell e Whitehead nei Principia; ulteriori sistemi assiomatici sono considerati da David Hilbert. Una svolta si ha nel 1935 con un lavoro del logico tedesco Gerhard Gentzen (1909-1945), Untersuchungen über das logische Schliessen (Ricerche sulla deduzione logica) che costituisce una pietra miliare nella storia della logica novecentesca.

Consapevole che la formalizzazione della deduzione logica a opera dei suoi predecessori si discostava di molto “dalle forme di deduzione usate nella pratica delle dimostrazioni matematiche”, Gentzen sviluppa un calcolo della deduzione naturale per la logica classica (NK) e per la logica intuizionista (NJ) in modo da renderlo “il più vicino possibile all’effettivo ragionamento”. La prima formulazione della logica intuizionista, dove non vale il principio del terzo escluso, risale a Arend Heyting (1898-1980) nel 1930. (Nel 1933 Gödel aveva mostrato che la logica intuizionista è interpretabile in una delle logiche modali standard, S4. E Saul Kripke nel 1965 proporrà una semantica per la logica intuizionista che è simile in spirito a quella per S4.) L’idea di Gentzen per il suo calcolo di deduzione naturale era la decomposizione delle regole d’inferenza per ogni costante logica c (connettivi e quantificatori) in passi atomici di due tipi, introduzione ed eliminazione .

La regola d’introduzione per c stabilisce una condizione per inferire come conclusione una formula che contiene c come costante logica principale; simmetricamente, la regola di eliminazione per c stabilisce quale inferenza può essere tratta da una formula che contiene c come costante logica principale: ciascuna regola è tale che non si possono immaginare altre regole più basilari in termini di cui la regola sia derivabile. Gentzen formula un teorema (il cosiddetto Hauptsatz) per cui ogni dimostrazione del calcolo può essere trasformata in una dimostrazione normale nella quale non ci sono parti superflue: una regola d’introduzione non è mai seguita da una di eliminazione per la stessa costante logica. Ma per Gentzen il calcolo della deduzione naturale non offriva il contesto sintattico più comodo (specie per LK) per dimostrare l’Hauptsatz, che per il calcolo NJ e NK sarà dimostrato da Dag Prawitz solo nella prima metà degli anni Sessanta. Gentzen introduce un nuovo calcolo di deduzione, equivalente al primo, nella doppia versione classica (LK) e intuizionista (LJ), chiamato calcolo dei sequenti .

Un sequente è un’espressione della forma , dove e sono successioni (finite) di formule dette rispettivamente antecedente e conseguente e “” denota la relazione binaria di deducibilità tra successioni di formule. Dati  = A₁,...,A_n e  = B₁,...,B_m dove n, m ≥ 1, significa informalmente:

A₁ e…e A_n implica B₁ o...o B_m

Se m = 0, A₁,..., A_n significa che A₁ e…e A_n porta a una contraddizione; se n = 0, B₁,..., B_m significa (B₁ o...o B_m); se m = n = 0, significa che c’è una contraddizione. Un’inferenza è una relazione tra sequenti S₁, S₂, S, della forma:

oppure

Una dimostrazione è data dall’applicazione delle regole d’inferenza che termina con il sequente dimostrato e inizia con un sequente della forma A A. Nel calcolo dei sequenti tutte le regole d’inferenza che governano i connettivi ed i quantificatori, sono regole d’introduzione, mentre una particolare regola, chiamata regola del taglio:

esprime la transitività dell’implicazione e simula gli effetti di tutte le regola di eliminazione della deduzione naturale. Questa regola corrisponde all’utilizzo di lemmi o di proposizione intermedie (la formula A) nel corso di una dimostrazione, cioè cattura un procedimento fondamentale in matematica. La differenza tra la logica intuizionista e la logica classica consiste ora semplicemente in una diversa relazione “”: in LK, “” è una relazione a m + n posti, mentre in LJ “” è una relazione a m + 1 posti, ossia ogni sequente di LJ può contenere al massimo una formula nel conseguente. Un sequente intuizionista è quindi un “processo” che ha più assunzioni (inputs) e una sola conclusione (output).

L’Hauptsatz (o teorema di eliminazione del taglio) per il calcolo LJ e LK afferma che il calcolo con la regola di taglio è conservativo sul calcolo senza la regola di taglio: ogni dimostrazione π di un sequente che usa la regola del taglio può essere trasformata in una dimostrazione π’ dello stesso sequente senza la regola del taglio. In altre parole, π’ esplicita tutta l’informazione contenuta implicitamente in π. Questo teorema traccia il confine tra un calcolo logico e la più ampia nozione di sistema formale. Come corollario si ottiene la proprietà della sottoformula: in una dimostrazione senza taglio ogni formula che occorre nelle premesse è una sottoformula di una formula occorrente nel sequente dimostrato. Questa proprietà permette di dimostrare la coerenza del calcolo logico (il sequente non è dimostrabile). Sfruttando il teorema di eliminazione del taglio, inoltre, risulta molto agevole ottenere il teorema di Herbrand (1930), che permette di riduce la dimostrabilità di una formula con quantificatori alla dimostrabilità di una formula senza quantificatori nel calcolo proposizionale. Nel calcolo dei sequenti per la logica classica e intuizionista esistono regole esprimibili senza un esplicito riferimento a connettivi. Gentzen chiama queste regole strutturali per indicare il fatto che esse riguardano la struttura di un sequente. Per Gentzen le regole strutturali sono quattro: la regola d’indebolimento, della contrazione, dello scambio e del taglio, ma successivamente nella letteratura si è inteso per regole strutturali solo le prime tre regole, considerando lo status specifico della regola del taglio nel calcolo dei sequenti. Le regole strutturali determinano il comportamento sintattico e lo stile di deduzione di una logica, nel senso che dato l’insieme RS = {indebolimento, contrazione, scambio} e considerando tutte le possibili combinazioni degli elementi, abbiamo 2³ = 8 insiemi diversi e quindi 8 logiche diverse. Recentemente l’eliminazione delle regole d’indebolimento e di contrazione ha portato alla scoperta della logica lineare, da parte di J.Y. Girard nel 1986, nella quale sono definiti connettivi più primitivi dei connettivi classici. Questo si traduce in una nuova concezione geometrica delle dimostrazioni logiche concepite come grafi, nei quali i vertici sono etichettati da formule. Inoltre è possibile interpretare l’eliminazione del taglio in termini di iterazioni di operatori in C*-algebre. Una dimostrazione è una struttura dinamica all’interno della quale circola l’informazione.