Logica matematica

La logica matematica è lo studio della logica formale all'interno della matematica. Essa rappresenta un insieme di discipline che si pongono domande fondamentali su come funziona l’intera struttura della matematica. In termini più precisi, la logica matematica studia i sistemi formali, analizzando i modi in cui concetti intuitivi come la dimostrazione e la computazione possano essere rappresentati e formalizzati all’interno dei fondamenti della matematica. Si occupa quindi delle parti della logica che possono essere modellate matematicamente.

In passato, per riferirsi a questa disciplina venivano usati termini come logica simbolica (in contrapposizione alla logica filosofica) e metamatematica, termine che oggi si applica più specificamente ad alcuni aspetti della teoria della dimostrazione.

Le principali sottoaree della logica matematica includono la teoria dei modelli, la teoria della dimostrazione, la teoria degli insiemi e la teoria della ricorsione (o teoria della calcolabilità). La ricerca in questo campo si concentra spesso sulle proprietà matematiche dei sistemi logici formali, il loro potere espressivo o deduttivo, ma anche sull’uso della logica per descrivere il corretto ragionamento matematico e stabilire solide basi teoriche per tutta la matematica. Un importante settore collegato è la teoria delle categorie, che studia le relazioni, le trasformazioni (dette “mappe”) e i collegamenti tra oggetti matematici. Nella teoria dei modelli, invece, un modello è una struttura concreta nella quale un insieme di regole astratte, cioè gli assiomi, risulta vero.

Lo studio dei fondamenti della matematica iniziò alla fine del XIX secolo con lo sviluppo di sistemi assiomatici per la geometria, l’aritmetica e l’analisi matematica. All’inizio del XX secolo esso fu fortemente influenzato dal programma di David Hilbert, che mirava a dimostrare la coerenza delle teorie fondamentali. I risultati ottenuti da Kurt Gödel, Gerhard Gentzen e altri matematici portarono però a una revisione profonda di questi obiettivi. In particolare, la scoperta dei teoremi di incompletezza di Gödel dimostrò che, all’interno di qualsiasi sistema matematico sufficientemente potente, esisteranno sempre affermazioni indecidibili, cioè né dimostrabili né confutabili. Questa scoperta diede origine allo studio dell’indecidibilità e mostrò i limiti intrinseci dei sistemi formali.

I lavori nella teoria degli insiemi evidenziarono inoltre che quasi tutta la matematica ordinaria può essere formalizzata in termini di insiemi, anche se esistono teoremi che non possono essere dimostrati nei più comuni sistemi assiomatici. La ricerca contemporanea sui fondamenti della matematica si concentra spesso sul determinare quali parti della matematica possano essere formalizzate in specifici sistemi formali, come avviene nella matematica inversa, piuttosto che nel tentativo di trovare un unico sistema capace di contenere tutta la matematica.

Storia

Logica matematica è il nome assegnato da Giuseppe Peano a quella che era già nota come logica simbolica o anche formale. Si tratta sostanzialmente della logica di Aristotele, ma viene scritta nei termini dell'algebra astratta e della combinatoria.

Dei tentativi di trattare le operazioni della logica formale con modalità simboliche o algebriche furono effettuati da alcuni dei matematici con più spiccate attitudini filosofiche, come Gottfried Leibniz e Johann Heinrich Lambert; i loro sforzi, però, rimasero quasi sconosciuti e isolati. Furono George Boole e il suo continuatore, Augustus De Morgan, che, intorno alla metà del XIX secolo, proposero, per il trattamento della logica, alcune modalità matematiche sistematiche (di natura non-quantitativa). In tal modo la dottrina tradizionale, aristotelica, della logica, veniva riformata e completata; in questo modo, si sviluppava anche uno strumento adeguato per l'indagine dei concetti fondamentali della matematica. Lo sviluppo di questa "nuova" logica ha condotto ad affrontare problemi che sono sfociati in controversie fondazionali ampiamente dibattute fra il 1900 e il 1925 e che sarebbe fuorviante considerare ricomposte; in ogni caso, la filosofia della matematica ha ricevuto una profonda chiarificazione dalle acquisizioni della logica matematica.

Mentre lo sviluppo tradizionale della logica classica pone forte enfasi sulla forma delle argomentazioni, l'atteggiamento della logica matematica dei nostri giorni potrebbe essere riassunto con la frase studio combinatorio del contenuto. Questa espressione copre sia i suoi atteggiamenti sintattici (ad es. individuare in un linguaggio formale una stringa da inviare a un programma compilatore perché la trascriva come una sequenza di istruzioni per il computer), sia i suoi atteggiamenti semantici (costruire specifici modelli o interi insiemi di stringhe, nella teoria dei modelli).

Alcune pubblicazioni determinanti sono state la Begriffsschrift (Ideografia) di Gottlob Frege e i Principia Mathematica di Bertrand Russell e Alfred North Whitehead.

Argomenti della logica matematica

Tra le aree principali della logica matematica vi sono la teoria dei modelli, la teoria della dimostrazione e la teoria della ricorsione. A queste talora viene aggiunta anche la Teoria degli insiemi. Molte sono le sovrapposizioni con l'informatica teorica, fin dai lavori dei pionieri di questa disciplina, come Alan Turing e Alonzo Church, che erano matematici e logici. Lo studio della semantica dei linguaggi di programmazione è derivato dalla teoria dei modelli, come è accaduto alla verifica dei programmi, in particolare alla verifica dei modelli.

L'isomorfismo di Curry-Howard tra dimostrazioni e programmi si collega alla teoria della dimostrazione; per queste questioni sono significative anche la logica intuizionista e la logica lineare. Calcoli come il lambda calcolo e la logica combinatoria oggi sono studiati principalmente come linguaggi di programmazione idealizzati.

Nel senso speculare inoltre l'informatica contribuisce alla logica sviluppando strumenti per la verifica automatica delle dimostrazioni e anche per l'individuazione delle dimostrazioni: tra questi i dimostratori automatici dei teoremi e gli strumenti della programmazione logica.

Teoremi significativi

• Teorema di semidecidibilità
• Teorema di completezza (forte)
• Teorema di completezza (debole)
• Teoremi di incompletezza di Gödel
• Teorema di Löwenheim-Skolem (debole)
• Teorema di compattezza (semantico)
• Teorema di compattezza (sintattico)
• Lemma di Zorn
• Lemma di König

Alcuni risultati fondamentali

• Le dimostrazioni computative della validità universale delle formule della logica del primo ordine possono essere sottoposte alla verifica algoritmica della loro validità. Con un'espressione tecnica si dice che il linguaggio delle dimostrazioni è ricorsivo primitivo. Essenzialmente questo equivale al teorema di completezza di Gödel; esso però in genere viene formulato per chiarire che esso non ha nulla a che fare con gli algoritmi.
• Il linguaggio delle formule valide della logica del primo ordine non è decidibile, bensì semidecidibile, questo implica che esiste un algoritmo in grado di valutare la validità di una formula. Nel caso in cui la formula sia valida l'algoritmo è in grado di terminare restituendo come prova la dimostrazione della sua validità, in caso contrario, se la formula non è valida, l'algoritmo non è in grado di accorgersene e continua a eseguire calcoli (si dice che diverge), senza mai fornire una risposta. Per questo il linguaggio delle formule si dice ricorsivamente enumerabile.
• Il linguaggio di tutte le formule universalmente valide della logica del secondo ordine non è neppure ricorsivamente enumerabile. Questa è una conseguenza del teorema di incompletezza di Gödel, quindi un eventuale algoritmo che prende in input una formula potrebbe divergere anche nel caso in cui la formula sia valida.
• Eliminazione dei tagli nel calcolo dei sequenti.
• L'indipendenza logica dell'ipotesi del continuo dimostrata da Paul Cohen nel 1963.

Bibliografia

• Stephen Cole Kleene: Introduction to Metamathematics. North-Holland, 1950.
• Andrea Asperti, Agata Ciabattoni: Logica a Informatica (2 ed.). McGraw-Hill, 2005.
• Evert Willem Beth: I fondamenti logici della matematica. Feltrinelli, 1963.
• George Boolos, Richard Jeffrey: Computability and Logic (3 ed.). Cambridge University Press, 1989.
• Ettore Casari: Lineamenti di logica matematica (3 ed.). Feltrinelli, 1964.
• Vincenzo Manca, Logica Matematica, Bollati Boringhieri, 2000.
• Elliott Mendelson, Introduzione alla Logica Matematica, Bollati Boringhieri, 1972.
• Dario Palladino: Corso di Logica. Introduzione elementare al calcolo dei predicati, Carocci, 2002.
• Dario Palladino: Logica e teorie formalizzate. Completezza, incompletezza, indecidibilità, Carocci, 2004.
• Willard Van Orman Quine: Manuale di logica (4 ed.). Feltrinelli, 1970.
• Joseph R. Shoenfield: Logica matematica. Bollati Boringhieri, 1980.
• Alfred Tarski: Introduzione alla logica. Bompiani, 1969.
• Achille C. Varzi, John Nolt, Dennis Rohatyn: Logica (2 ed.). McGraw-Hill, 2007.

Voci correlate

• Assioma (matematica)
• Base di Herbrand
• Calcolo dei sequenti
• Elenco (logica formale)
• Logica
• Logica della computabilità
• Logica intuizionista
• Logica dei predicati
• Logica modale
• Logica dinamica
• Model checking
• Teorema di deduzione

Altri progetti

Altri progetti

• Wikibooks
• Wikizionario
• Wikiversità
• Wikimedia Commons

• Wikibooks contiene testi o manuali sulla logica matematica
• Wikizionario contiene il lemma di dizionario «logica matematica»
• Wikiversità contiene una materia sulla logica matematica
• Wikimedia Commons contiene immagini o altri file sulla logica matematica

Collegamenti esterni

• Abraham Robinson, Logica matematica, in Enciclopedia del Novecento, Istituto dell'Enciclopedia Italiana, 1978.
• logica matematica, in Dizionario di filosofia, Istituto dell'Enciclopedia Italiana, 2009.
• (EN) G.E. Hughes e Morton L. Schagrin, formal logic, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.
• (EN) Opere riguardanti Mathematical logic, su Open Library, Internet Archive.
• (EN) Mathematical logic around the world, su world.logic.at. URL consultato il 5 marzo 2015 (archiviato dall'url originale l'8 aprile 2007).
• (EN) Polyvalued logic, su home.swipnet.se. URL consultato il 24 febbraio 2005 (archiviato dall'url originale il 5 giugno 2009).
• Breve storia della logica (PDF), su ulisse.sissa.it.
• (EN) Computability logic Recente orientamento nella logica matematica, che si propone di spostarla dalla teoria della verità verso la teoria della computabilità.