Logica matematica

La logica matematica è il settore della matematica che studia i sistemi formali dal punto di vista del modo di codificare i concetti intuitivi della dimostrazione e di computazione come parte dei fondamenti della matematica. Essa si occupa delle parti della logica che possono essere modellate matematicamente. Altri termini utilizzati spesso nel passato sono logica simbolica (termine contrapposto a logica filosofica) e metamatematica, termine che ora si applica più specificamente a taluni aspetti della teoria della dimostrazione.

Storia[modifica | modifica wikitesto]

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[modifica | modifica wikitesto]

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[modifica | modifica wikitesto]

Alcuni risultati fondamentali[modifica | modifica wikitesto]

  • 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[modifica | modifica wikitesto]

Voci correlate[modifica | modifica wikitesto]

Altri progetti[modifica | modifica wikitesto]

Collegamenti esterni[modifica | modifica wikitesto]

Controllo di autoritàThesaurus BNCF 7927 · LCCN (EN) sh85003435 · GND (DE) 4037951-6 · BNE (ES) XX525820 (data) · BNF (FR) cb11965690r (data) · J9U (EN, HE) 987007293932405171 · NDL (EN, JA) 00565709
  Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica
Estratto da "https://it.wikipedia.org/w/index.php?title=Logica_matematica&oldid=137324989"