Logica formale: Problemi e prove classiche

Titolo originale:

Formal Logic: Classical Problems and Proofs

Contenuto del libro:

La logica è - indiscutibilmente - tutta una questione di dimostrazione, ma le prove possono essere "costose", spesso impossibili, e oggi la maggior parte di esse sono delegate a dimostratori (parzialmente) automatici, cioè ai cosiddetti risolutori SAT, software basati sul problema della soddisfabilità (booleana), o SAT. Questo è il duale del problema della validità (booleana), o VAL, al centro della concezione del computer digitale attraverso il Entscheidungsproblem di Hilbert e la Macchina di Turing universale. Mentre questi problemi - VAL in misura significativamente minore rispetto a SAT - sono presenti nei libri di testo di logica introduttiva rivolti a studenti di informatica, sono in gran parte o del tutto assenti nei libri di testo rivolti a studenti di matematica o di filosofia.

Logica formale: problemi e prove classiche corregge questo - a nostro avviso - errato stato di cose, fornendo le basi della logica formale classica dal punto di vista centrale di un linguaggio formale, o informatico, che si distingue dagli altri linguaggi formali o informatici per la sua capacità di preservare la verità, fornendo così potenzialmente soluzioni a problemi decisionali formulati in termini di VAL e/o SAT. Questo aspetto fondamentale della logica classica, la conservazione della verità, viene elaborato a partire da tre principali semantiche formali, ovvero la semantica tarskiana, quella di Herbrand e quella algebrica (booleana), che a loro volta, tramite i risultati di adeguatezza per la logica del primo ordine standard, sono alla base dei principali sistemi di dimostrazione diretta e indiretta, o di confutazione, associati rispettivamente a VAL e SAT.

Non concentrandosi sulla storia della logica classica, questo libro fornisce comunque discussioni e citazioni di passaggi centrali sulle sue origini e sul suo sviluppo, in particolare da una prospettiva filosofica. Non essendo un libro di logica matematica, affronta la logica formale da una prospettiva essenzialmente matematica. Orientato verso un approccio computazionale, con SAT e VAL come spina dorsale, è quindi un'introduzione alla logica che copre gli aspetti essenziali delle tre branche della logica, ovvero quella filosofica, quella matematica e quella computazionale.