Logica matematica

Da Wikipedia, l'enciclopedia libera.

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 sorgente]

Logica matematica è il nome assegnato da Giuseppe Peano a quella che era nota anche come logica simbolica o anche formale. In buona sostanza è ancora la logica di Aristotele, ma viene scritta nei termini dell'algebra astratta e della combinatoria.

Dei tentativi di trattare le operazioni delle 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; però i loro sforzi 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 modalità matematiche sistematiche (naturalmente di natura non-quantitativa). In tal modo la dottrina tradizionale, aristotelica della logica, veniva riformata e completata; inoltre risultava sviluppato 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 (vedi elenco degli articoli di logica) 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 (Notazione dei concetti) di Gottlob Frege e i Principia Mathematica di Bertrand Russell.

Argomenti della logica matematica[modifica | modifica sorgente]

Le aree principali della logica matematica includono la teoria dei modelli, teoria della dimostrazione e la teoria della ricorsione.
A queste talora viene aggiunta anche la Teoria degli insiemi. Essa possiede molte sovrapposizioni con l'informatica, fin dai lavori dei pionieri di questa disciplina, come Alan Turing, i quali 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 la individuazione delle dimostrazioni: tra questi i dimostratori automatici dei teoremi e gli strumenti della programmazione logica.

Teoremi significativi[modifica | modifica sorgente]

Alcuni risultati fondamentali[modifica | modifica sorgente]

  • Le dimostrazioni computative della validità universale delle formule della logica del primo ordine possono essere sottoposte alla verifica algoritmica della loro validità. Con una 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.

Bibliografia[modifica | modifica sorgente]

Voci correlate[modifica | modifica sorgente]

Collegamenti esterni[modifica | modifica sorgente]

matematica Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica