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.

Sebbene molti siano indotti a pensare che la logica matematica sia la matematica della logica, è più giustificato affermare che essa è la logica applicata alla 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.

[modifica] Storia

Logica matematica è il nome assegnato da Giuseppe Peano a quella che era nota anche come logica simbolica. In buona sostanza è ancora la logica di Aristotele, ma si pone dal punto di vista che considera la notazione con la quale viene scritta come branca 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 Lambert; purtroppo 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.

[modifica] Argomenti della logica matematica

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 assiomatica 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.

[modifica] Teoremi significativi

• Teorema di semidedicibilità
• Teorema di completezza (forte)
• Teorema di completezza (debole)
• Teorema di Löwenheim-Skolem (debole).
• Regola 1,n
• Regola 2
• Teorema di compattezza (semantico)
• Teorema di compattezza (sintattico)
• Lemma di Zorn
• Lemma di König

[modifica] Alcuni risultati fondamentali

• Le dimostrazioni putative 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 in modo da 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.

• La independenza logica della ipotesi del continuo dimostrata da Paul Cohen nel 1963.

[modifica] Bibliografia

• Anne Sjerp Troelstra, H. Schwichtenberg (2000). Basic Proof Theory (2nd ed.). Cambridge University Press. ISBN 0521779111.
• George Boolos, Richard Jeffrey (1989). Computability and Logic (3rd ed.). Cambridge University Press. ISBN 0521007585.
• Diego Filotto(2005). Dalla grammatica alla logica (1 ed.). Armando Editore ISBN 88-8358-715-4.

[modifica] Voci correlate

• Logica
• Logica della computabilità
• Semantica dei giochi
• Logica della dimostrabilità
• Logica della interpretabilità
• Calcolo dei sequenti
• Logica intuizionista
• Logica dei predicati
• Assioma (matematica)
• Model checking

[modifica] Collegamenti esterni

• (EN) Mathematical logic around the world
• (EN) Polyvalued logic
• (EN) Computability logic Recente orientamento nella logica matematica, che si propone di spostarla dalla teoria della verità verso la teoria della computabilità.