Usando due volte l'elemento (8), ossia il Modus Ponens, è sufficiente mostrare che il set {A, C, ¬B, ¬C, ¬D} è incoerente. Questo accade perché contiene sia C che ¬C come membri, il che genera una contraddizione. La dimostrazione dell'incoerenza di un sistema rappresenta uno degli aspetti più fondamentali della logica proposizionale, e i teoremi di completezza e correttezza si inseriscono in questo contesto come proprietà centrali per qualsiasi sistema di logica proposizionale.
Il Teorema di Correttezza afferma che la logica proposizionale (PL) è "corretta", nel senso che ogni teorema provabile in PL è una tautologia. In altre parole, se un teorema A può essere dimostrato all'interno di un sistema PL, allora A è una verità generale, valida in tutte le interpretazioni. Inoltre, se A è provabile da un insieme di ipotesi Γ, allora Γ implica tautologicamente A. Questa proprietà è essenziale per garantire che i sistemi formali, come PL, possano produrre solo verità universali.
Il Teorema di Completezza, d'altra parte, afferma il contrario: se A è una tautologia, allora A ha una prova in PL. Inoltre, se A è una conseguenza tautologica di un insieme di ipotesi Γ, allora Γ ⊢ A. In altre parole, il sistema PL, con i suoi quattro schemi assiomatici (PL1-PL4) e l'unica regola di inferenza del Modus Ponens, è sufficientemente potente da fornire una prova per tutte le tautologie. Questo risultato è veramente straordinario, in quanto implica che la logica proposizionale sia sia corretta che completa.
I teoremi di correttezza e completezza insieme esprimono una simmetria fondamentale: la soddisfacibilità e la coerenza sono equivalenti. Inoltre, l'implicazione tautologica (⊧) è equivalente alla provabilità (⊢). In altre parole, Γ ⊢ A è equivalente a Γ ⊧ A. Nel caso speciale in cui Γ è l'insieme vuoto, ⊢ A è equivalente a ⊧ A. Ciò significa che A ha una prova in PL se e solo se A è una tautologia.
La Completezza apre la porta a una nuova regola di inferenza derivata per PL, chiamata Implicazione Tautologica. Se A1, A2, ..., Ak ⊧ B, allora l'implicazione tautologica (TAUT) è ammissibile come regola derivata per le prove PL: A1, A2, ..., Ak ⊢ B. Per dimostrare che TAUT è una regola di inferenza ammissibile, si nota che il Teorema di Completezza implica che A1, A2, ..., Ak ⊢ B. Quindi, utilizzando il Teorema di Deduzione, si arriva alla conclusione che ⊢ A1 → A2 → ... → Ak → B. Successivamente, se le ipotesi A1, ..., Ak sono state derivate, l'uso del Modus Ponens consente di derivare B. La Sillogismo Ipotetico e il Modus Tollens (e anche il Modus Ponens) sono casi speciali della regola di Implicazione Tautologica. In effetti, i Teoremi di Correttezza e Completezza mostrano che la regola di Implicazione Tautologica è la più forte possibile per la logica proposizionale.
Sia il Teorema di Correttezza che quello di Completezza si compongono di due parti che implicano reciprocamente l'una l'altra. Per esempio, partendo dalla parte (a) del Teorema di Correttezza, si dimostra facilmente che la parte (b) è vera. Allo stesso modo, per il Teorema di Completezza, si segue un ragionamento simile: se Γ ⊧ A, allora Γ ∪ {¬A} è insoddisfacente, e questo porta alla conclusione che Γ ⊢ A.
La dimostrazione del Teorema di Correttezza inizia supponendo che Γ sia un insieme di formule e che Γ ⊢ A. Per dimostrare che Γ ⊧ A, si procede per induzione, mostrando che per ogni formula Ai che compone la prova di A, φ(Ai) = T per ogni i. Se Ai è un assioma di PL, è una tautologia, quindi φ(Ai) = T. Se A è un membro di Γ, allora φ(Ai) = T per definizione. Infine, se Ai è inferita tramite Modus Ponens, si usa l'ipotesi di induzione per dimostrare che φ(Ai) = T. Questo conclude la prova per induzione.
La parte (a) del Teorema di Correttezza stabilisce che se Γ è incoerente, allora Γ ⊢ A e Γ ⊢ ¬A. Di conseguenza, per ogni assegnazione di verità φ che soddisfa Γ, φ(A) = T e φ(¬A) = T, il che è impossibile. Pertanto, non esiste un'assegnazione di verità che soddisfi Γ, e quindi Γ è insoddisfacente. Questo completa la dimostrazione del Teorema di Correttezza.
Il Teorema di Completezza, che viene dimostrato successivamente in modo più complesso, si basa sulla costruzione di un insieme completo e consistente di formule che estende Γ, come espresso nel Teorema di Lindenbaum. Questo insieme è costruito in modo tale che, per ogni formula A, o A è in Π o ¬A è in Π. La completezza di Π garantisce che ogni formula ha una prova nel sistema, rendendo il sistema veramente "completo" nel suo potenziale di provare tautologie.
In sintesi, i teoremi di correttezza e completezza non solo forniscono la base teorica della logica proposizionale, ma mostrano anche come questa logica si comporta in relazione alle proprietà fondamentali della verità e della provabilità. La loro importanza non risiede solo nel fornire una giustificazione formale per i risultati, ma anche nell'affermare che ogni tautologia ha una prova, e ogni prova è una tautologia. In altre parole, la logica proposizionale è sia potente che affidabile.
Qual è il legame tra cardinalità, modelli e i teoremi di Löwenheim-Skolem?
Nel contesto della logica del primo ordine, i concetti di cardinalità e di modelli rivestono un ruolo centrale per la comprensione dei teoremi fondamentali che regolano la teoria dei modelli. Tra questi, i teoremi di Löwenheim-Skolem sono tra i più rilevanti, in quanto pongono delle limitazioni sull'esistenza di modelli di determinate teorie e forniscono una profonda intuizione sul comportamento delle teorie di logica in relazione alla cardinalità delle strutture che le interpretano.
Nel caso di una teoria consistente, ovvero una teoria che non porta a contraddizioni, la compattezza e i teoremi di Löwenheim-Skolem affermano che se una teoria ha modelli di dimensioni arbitrariamente grandi, essa ammette anche un modello infinito. Questo è un risultato fondamentale che stabilisce un legame tra la consistenza di una teoria e l’esistenza di modelli infiniti.
L'analisi delle cardinalità dei modelli di una teoria ci aiuta a capire come le teorie possano essere interpretate in strutture di dimensioni diverse. In particolare, quando consideriamo teorie con linguaggi numerabili e modelli numerabili, possiamo osservare che se una teoria è numerabilmente categorica (ovvero ha esattamente un modello numerabile, up to isomorfismo), essa sarà completa, ossia ogni frase che può essere derivata dalla teoria sarà vera o falsa in ogni modello della teoria.
Un aspetto sorprendente dei teoremi di Löwenheim-Skolem è che una teoria che implica l'esistenza di insiemi non numerabili può comunque avere modelli numerabili. Questo fenomeno è noto come il "paradosso di Skolem", che, pur non essendo un vero paradosso, appare tale a causa del contrasto tra l'intuizione di un insieme numerabile e le conseguenze di una teoria che afferma l'esistenza di insiemi di cardinalità maggiore. Nel caso della teoria degli insiemi ZF, ad esempio, la sua coerenza implica l'esistenza di un modello numerabile, ma in questo modello l'interpretazione di "insiemi infiniti" sarà diversa da quella del mondo reale.
Inoltre, un aspetto significativo di questi risultati riguarda la possibilità che una teoria abbia modelli non standard, come nel caso degli interi. Sebbene la teoria degli interi sia completa, essa non è numerabilmente categorica, come dimostrato dal fatto che esistono modelli numerabili non isomorfi che soddisfano la stessa teoria.
Tuttavia, la teoria dei modelli non si limita solo a considerare le proprietà delle teorie numerabili. Per linguaggi non numerabili, la definizione di cardinalità di un linguaggio L è fondamentale per determinare la dimensione di eventuali modelli che interpretano una teoria. Se L è numerabile, la cardinalità di un modello di una teoria sarà al massimo quella di L, ma se L è non numerabile, la situazione cambia e diventa possibile che la teoria ammetta modelli di cardinalità arbitraria.
Un altro risultato interessante e di grande importanza nella logica del primo ordine è la versione modificata del teorema di completezza che si applica ai linguaggi non numerabili. In pratica, se una teoria è consistente e il suo linguaggio è numerabile, allora essa avrà un modello di cardinalità che non supera quella del linguaggio stesso. Questo implica che la nozione di "completamento" di una teoria può essere estesa anche a contesti in cui i linguaggi sono molto più complessi e di cardinalità più alta.
In sintesi, i teoremi di Löwenheim-Skolem non solo stabiliscono un legame tra la cardinalità di un modello e le caratteristiche della teoria che lo definisce, ma evidenziano anche come una teoria possa ammettere modelli numerabili, nonostante contenga affermazioni che riguardano insiemi non numerabili. La capacità di una teoria di ammettere modelli di diverse cardinalità implica una notevole flessibilità nelle interpretazioni logiche, ma allo stesso tempo suggerisce che la logica del primo ordine, pur potente, non può sempre catturare tutte le sfumature della realtà matematica, specialmente quando si trattano teorie che coinvolgono l'infinitamente grande o l'infinitamente piccolo.
La Decidibilità nelle Logiche Proposizionali e di Primo Ordine: Algoritmi e Conseguenze Logiche
Nella logica proposizionale, gli algoritmi di parsing hanno un ruolo fondamentale nella costruzione degli alberi di analisi. Questi algoritmi non solo analizzano la sintassi delle formule, ma possono anche determinare se una formula è una tautologia, cioè se è vera in ogni possibile interpretazione. Il teorema V.35 afferma che l'insieme delle tautologie è decidibile. La prova di questo teorema si basa su un algoritmo che prima verifica la correttezza sintattica della formula proposta e, successivamente, impiega il metodo delle tavole della verità per determinare se la formula è una tautologia. Il metodo delle tavole della verità è, infatti, uno degli strumenti algoritmici principali per il trattamento delle formule proposizionali, e la sua applicazione permette di decidere se una formula è valida o soddisfacibile in modo sistematico.
Un concetto chiave nella logica proposizionale è la soddisfacibilità di un insieme di formule. La soddisfacibilità di un insieme di formule Γ, cioè la possibilità di assegnare valori di verità in modo che tutte le formule di Γ siano vere simultaneamente, è anch'essa decidibile, come afferma il teorema V.36. Esistono algoritmi che possono determinare se un insieme di formule Γ è soddisfacibile, e altrettanto se una formula A è una conseguenza logica di Γ (indicato con Γ ⊧ A). L'algoritmo che affronta questo problema inizia con la verifica della correttezza sintattica di Γ e poi applica il metodo delle tavole della verità per determinare la soddisfacibilità dell'insieme. Se l'insieme Γ è soddisfacibile, l'algoritmo stabilisce che esiste un'assegnazione di verità che rende vere tutte le formule di Γ.
Quando si trattano insiemi infiniti di formule, come nel caso delle formule computazionalmente enumerabili, la situazione si complica. Il teorema V.37 mostra che, data una sequenza di formule proposizionali computazionalmente enumerabili, l'insieme delle conseguenze tautologiche di Γ è computazionalmente enumerabile. Questo significa che, pur non essendo decidibile in modo completo, è possibile enumerare tutte le formule che sono conseguenze tautologiche di Γ. L'algoritmo N descritto nella prova di questo teorema cerca, passo dopo passo, attraverso l'enumerazione di Γ, se una formula A è una conseguenza tautologica di Γ, accettando A non appena viene identificato un sottoinsieme di Γ che la implica tautologicamente.
Un punto cruciale, tuttavia, è che non sempre l'insieme delle conseguenze logiche di un insieme di formule decidibile è anch'esso decidibile. Il teorema V.37 fornisce una dimostrazione che quando l'insieme Γ è computazionalmente enumerabile, l'insieme delle conseguenze logiche di Γ non è sempre decidibile. Un esempio concreto di questa situazione si verifica quando si ha una formula come la disgiunzione ripetuta di una proposizione pi, che è tautologicamente equivalente alla proposizione pi stessa. L'algoritmo non sarà in grado di escludere tutte le possibili combinazioni di disgiunzioni di pi all'interno di Γ senza una verifica infinita.
Spostandoci verso la logica di primo ordine, la situazione si complica ulteriormente, ma gli algoritmi continuano a giocare un ruolo importante. In un linguaggio di primo ordine fisso, la logica delle formule e delle conseguenze logiche rimane computazionalmente enumerabile, anche se non sempre decidibile. Il teorema V.38 sottolinea che, data una lingua L finita, esistono algoritmi che possono decidere se una formula in L è sintatticamente corretta, se è un termine o una formula atomica corretta, e se una formula in L è sostituibile con un altro termine. Tuttavia, come nel caso della logica proposizionale, anche nella logica di primo ordine gli insiemi di formule possono non essere completamente decidibili, e ciò dipende dalla struttura dell'insieme di formule e dalla sua complessità.
In definitiva, la decidibilità e la computabilità sono due proprietà fondamentali nella logica formale, che determinano la possibilità di sviluppare algoritmi in grado di decidere il valore di verità delle formule o se una formula è una conseguenza logica di un insieme di altre formule. Tuttavia, la complessità degli insiemi di formule, in particolare quando sono infiniti o computazionalmente enumerabili, può impedire la completa decidibilità delle conseguenze logiche, rendendo necessario l'uso di metodi come le tavole della verità o l'enumerazione per identificare le conseguenze tautologiche.
Nel contesto di una logica di primo ordine, è importante comprendere che, sebbene esistano algoritmi per determinare la correttezza sintattica e per manipolare le formule, le proprietà come la soddisfacibilità o la validità possono diventare complessi da calcolare, specialmente quando si lavora con insiemi infiniti di formule. In questi casi, l'approccio algoritmico deve adattarsi alle caratteristiche specifiche della logica di primo ordine, utilizzando metodi di enumerazione e verifiche parziali per gestire la complessità dei problemi logici.

Deutsch
Francais
Nederlands
Svenska
Norsk
Dansk
Suomi
Espanol
Italiano
Portugues
Magyar
Polski
Cestina
Русский