Logica matematica/Calcolo delle proposizioni

Template:Logica matematica

Partiremo dal punto più semplice: la logica proposizionale, ovvero relativa alle proposizioni. In questo contesto si studiano funzionamento e proprietà dei connettivi logici, e non si analizza come si arriva al valore di verità delle formule atomiche.

Il potere espressivo di questo linguaggio è limitato: in esso, infatti, possiamo esprimere proposizioni che sono vere o false, ma non proprietà che possono valere o meno su uno/molti/tutti gli individui di una certa classe. Col basso potere espressivo si coniuga la decidibilità di questa logica. Presentiamo la sintassi e la semantica della logica proposizionale.

Sintassi

Introduciamo la nozione di linguaggio proposizionale $ℒ_{Σ}$ costruito su un alfabeto $Σ$ . Iniziamo con la definizione di alfabeto.

Alfabeto

Template:Definizione Nel seguito scriveremo $ℒ$ quando $Σ$ è chiaro dal contesto. Definiamo ora le formule di $ℒ$ .

Formule ben formate

Template:Definizione

Sottoformule

Template:Definizione Per evitare un uso eccessivo delle parentesi, introduciamo anche delle regole di precedenza tra i connettivi. Per le formule proposizionali, si usa la seguente convenzione: la massima precedenza a $\neg$ , poi, nell'ordine, ai connettivi $\land, \lor, \to$ e infine a $\leftrightarrow$ . Questo significa che, in assenza di parentesi, una formula ben formata va parentesizzata privilegiando le sottoformule i cui connettivi principali hanno precedenza più alta. A parità di precedenza, cioè se siamo in presenza di più occorrenze dello stesso connettivo, si assume che esso associ a destra, cioè la parentesizzazione va eseguita a partire dall'ultima occorrenza a destra del connettivo.

Simboli proposizionali occorrenti in una formula

Template:Definizione La funzione $s i m b$ restituisce l'insieme dei simboli proposizionali che occorrono in una formula. Essa è definita in $℘ 𝒫$ , cioè nell'inseme dei sottoinsiemi di $𝒫$ , dato che restituisce sempre un sottoinsieme di $𝒫$ .

Esempi

Le regole appena esposte indicano come formare le frasi del calcolo proposizionale. Le frasi ben formate nascono applicando a formule atomiche i connettivi logici come indicato, se non è possibile risalire a queste regole la frase non è una frase ben formata.

Le formule atomiche rappresentano frasi del tipo:

"Oggi splende il sole"
"Mi chiamo Giovanni"
"Tre è dispari"

cioè frasi che possono essere vere o false. Da esse verranno poi costruite le formule ben formate.

Esempi di frasi ben formate:

$((A \to B) \land (C \to D)) \to ((A \land C) \to (B \land D))$
$\neg A \to \neg \neg \neg A$
$A \leftrightarrow B \lor C$

mentre frasi invalide sono:

$A (B)$
$\to A \to B$
$A \to \land B$

I vari connettivi

Queste regole definiscono la sintassi che utilizzeremo per il calcolo delle proposizioni. Ora dobbiamo dare un significato a queste frasi.

Semantica

Dobbiamo definire come operano questi connettivi e lo faremo usando le tavole di verità. In questo modo potremo creare una semantica, ovvero dare un significato all'operazione che viene eseguita da ogni operatore.

Ci serviremo di variabili atomiche, ovvero indivisibili, che possono assumere solo valori di verità (vero o falso rispettivamente indicati con V o F o, se ci basiamo sulla lingua inglese T o F).

Sistema di valutazione

Template:Vedi anche Template:Definizione

Negazione

Template:Definizione Questo è di solito espresso in maniera concisa come:

$\neg (T) = F$
$\neg (F) = T$

cioè, la funzione di valutazione associata a un connettivo viene indicata col simbolo stesso del connettivo, e viene definita in forma tabellare mediante la tavola o tabella dei valori di verità per il connettivo come segue:

$\begin{matrix} A & \neg A \\ F & T \\ T & F \end{matrix}$

Tale tabella definisce la semantica dell'operazione di negazione. Se la frase $A$ è vera, la sua negazione è falsa; se la frase $A$ è falsa, la sua negazione è vera. Si tratta dell'unico connettivo unario, in quanto agisce su un'unica sentenza.

Evitando di presentare le funzioni ${𝒪 𝓅}_{\circ}$ della logica proposizionale per i connettivi binari, le presentiamo subito in forma di tabella dei valori di verità.

Per il fatto che l'insieme delle formule proposizionali è liberamente generato, ogni assegnazione $𝒱$ si estende a un'unica interpretazione o valutazione booleana.

Valutazione booleana

Template:Definizione

Il valore di verità di una formula $A$ dipende dall'assegnazione booleana a tutti i simboli proposizionali, inclusi quelli che non occorrono in $A$ . Tuttavia, per dare una valutazione booleana di $A$ basta dire come vengono valutati (interpretati) i simboli proposizionali di $A$ . Infatti, sia $A$ una formula proposizionale e sia $s i m b (A)$ l'insieme dei simboli proposizionali che occorrono in $A$ , per essi vale la seguente proprietà.

Teorema di equivalenza delle valutazioni

Se $𝒱_{1}$ e $𝒱_{2}$ sono due assegnazioni che coincidono su $s i m b (A)$ , allora $I_{𝒱_{1}} (A) = I_{𝒱_{2}} (A)$ .

Dimostrazione Procediamo per induzione strutturale.

(Passo Base) Osserviamo che l'asserto è vero per le formule $⊥$ e $⊤$ perché non contengono simboli proposizionali. Se $A \in 𝒫$ , allora abbiamo $𝒱_{1} (A) = 𝒱_{2} (A)$ e, per definizione, $I_{𝒱_{1}} (A) = I_{𝒱_{2}} (A)$ . Pertanto l'asserto vale per i simboli proposizionali.

(Passo Induttivo) Sia $A = (\neg B)$ . Abbiamo per $I_{𝒱_{1}}$ e $I_{𝒱_{2}}$ che $I_{𝒱_{1}} (\neg B) = {𝒪 𝓅}_{\neg} (I_{𝒱_{1}} (B))$ e $I_{𝒱_{2}} (\neg B) = {𝒪 𝓅}_{\neg} (I_{𝒱_{2}} (B))$ e dunque, poiché per ipotesi induttiva $I_{𝒱_{1}} (B) = I_{𝒱_{2}} (B)$ , segue che $I_{𝒱_{1}} (A) = I_{𝒱_{2}} (A)$ . Analogamente, sia $A = B \circ C$ con $\circ \in {\land, \lor, \to, \leftrightarrow}$ ; abbiamo $I_{𝒱_{1}} (B \circ C) = {𝒪 𝓅}_{\circ} (I_{𝒱_{1}} (B), I_{𝒱_{1}} (C))$ e $I_{𝒱_{2}} (B \circ C) = {𝒪 𝓅}_{\circ} (I_{𝒱_{2}} (B), I_{𝒱_{2}} (C))$ e, per ipotesi induttiva, $I_{𝒱_{1}} (B) = I_{𝒱_{2}} (B)$ e $I_{𝒱_{1}} (C) = I_{𝒱_{2}} (C)$ , segue che $I_{𝒱_{1}} (A) = I_{𝒱_{2}} (A)$ .

Soddisfacibilità

Formula soddisfatta

Template:Definizione

Formula soddisfacibile

Template:Definizione

Tautologia

Template:Definizione

Contraddizione

Template:Definizione

Tavole di verità

Dal teorema di equivalenza delle valutazioni segue che, per determinare se una formula proposizionale $A$ è soddisfacibile, tautologica o contraddittoria, basta costruire una tabella di valori di verità in cui compaiono $n + 1$ colonne, dove $n$ è il numero di simboli proposizionali distinti $A_{1}, . . ., A_{n}$ che compaiono in $A$ e nella n+1-esima colonna viene riportato il corrispondente valore $I_{𝒱} (A)$ . La tabella ha $2^{n}$ righe, tante quante sono le possibili assegnazioni distinte di valori di verità ai simboli di $A$ .

$\begin{matrix} A_{1} & . . . & A_{n} & I_{𝒱} (A) \\ F & . . . & F & I_{𝒱_{1}} (A) \\ . . . & . . . & . . . & . . . \\ T & . . . & T & I_{𝒱_{2^{𝓃}}} (A) \end{matrix}$

$A$ è una tautologia sse l'ultima colonna contiene solo $T$ , è soddisfacibile sse essa contiene almeno una $T$ , è contraddittoria sse essa contiene tutte $F$ .

Teorema

Una formula $A$ è una tautologia sse $\neg A$ è una contraddizione.

Dimostrazione

( $\Rightarrow$ ) Sia $A$ una tautologia. Per definizione, per ogni valutazione booleana $I_{𝒱}$ si ha che $I_{𝒱} (A) = T$ . Ora, per $\neg A$ si ha che:

$I_{𝒱} (\neg A) = {𝒪 𝓅}_{\neg} (I_{𝒱} (A)) = {𝒪 𝓅}_{\neg} (T) = F$

quindi, per ogni valutazione booleana $I_{𝒱}$ si ha che:

$I_{𝒱} (\neg A) = F$

dunque, $\neg A$ è una contraddizione.

Procedendo all'inverso, si dimostra analogamente che, se $\neg A$ è una contraddizione, allora $A$ è una tautologia:

( $\Leftarrow$ ) sia $\neg A$ una contraddizione. Per definizione, per ogni valutazione booleana $I_{𝒱}$ si ha che $I_{𝒱} (\neg A) = F$ . Ora, per $\neg A$ si ha che:

$I_{𝒱} (\neg A) = {𝒪 𝓅}_{\neg} (I_{𝒱} (A))$

quindi:

${𝒪 𝓅}_{\neg} (I_{𝒱} (A)) = F$

da cui, per la definizione di ${𝒪 𝓅}_{\neg}$ , si deduce che, per ogni valutazione booleana $I_{𝒱}$ :

$I_{𝒱} (A) = T$

dunque, $A$ è una tautologia.

Equivalenza logica

Implicazione logica

Template:Definizione

Equivalenza logica (Definizione)

Template:Definizione

Diamo qui di seguito una lista di formule tautologicamente equivalenti. L'equivalenza può essere facilmente verificata tramite tavole di verità.

$A \land A$	$\equiv$	$A$	idempotenza della congiunzione
$A \lor A$	$\equiv$	$A$	idempotenza della disgiunzione
$A \land (B \land C)$	$\equiv$	$(A \land B) \land C$	associatività della congiunzione
$A \lor (B \lor C)$	$\equiv$	$(A \lor B) \lor C$	associatività della disgiunzione
$A \leftrightarrow (B \leftrightarrow C)$	$\equiv$	$(A \leftrightarrow B) \leftrightarrow C$	associatività della doppia implicazione
$A \land B$	$\equiv$	$B \land A$	commutatività della congiunzione
$A \lor B$	$\equiv$	$B \lor A$	commutatività della disgiunzione
$A \leftrightarrow B$	$\equiv$	$B \leftrightarrow A$	commutatività della doppia implicazione
$A \land (B \lor C)$	$\equiv$	$(A \land B) \lor (A \land C)$	distributività della congiunzione sulla disgiunzione
$A \lor (B \land C)$	$\equiv$	$(A \lor B) \land (A \lor C)$	distributività della disgiunzione sulla congiunzione
$A \land (A \lor B)$	$\equiv$	$A$	assorbimento della congiunzione sulla disgiunzione
$A \lor (A \land B)$	$\equiv$	$A$	assorbimento della disgiunzione sulla congiunzione
$A \land ⊤$	$\equiv$	$A$	neutralità del vero nella congiunzione
$A \lor ⊤$	$\equiv$	$⊤$	assorbimento del vero nella disgiunzione
$A \lor ⊥$	$\equiv$	$A$	neutralità del falso nella disgiunzione
$A \land ⊥$	$\equiv$	$⊥$	assorbimento del falso nella congiunzione
$\neg \neg A$	$\equiv$	$A$	doppia negazione
$\neg (A \land B)$	$\equiv$	$\neg A \lor \neg B$	legge di De Morgan per la congiunzione
$\neg (A \lor B)$	$\equiv$	$\neg A \land \neg B$	legge di De Morgan per la disgiunzione
$A \lor \neg A$	$\equiv$	$⊤$	terzo escluso
$A \land \neg A$	$\equiv$	$⊥$	contraddizione
$A \to B$	$\equiv$	$\neg B \to \neg A$	contrapposizione
$A \to B$	$\equiv$	$\neg A \lor B$	trasformazione dell'implicazione in disgiunzione

Esercizi ed esempi

Relativamente alla legge del terzo escluso, il fatto che $A \lor \neg A$ sia sempre vero sembra del tutto intuitivo. In effetti, questa è una caratteristica della logica classica; in altre logiche, per esempio nella logica intuizionista, questo fatto non vale.

Intuitivamente ci si aspetta che, se una proposizione $A$ è logicamente equivalente a una proposizione $B$ , sostituendo $A$ al posto di $B$ in una formula $C$ , il valore di verità di $C$ non cambi.

Cerchiamo ora di rendere più precisa questa nozione. Indichiamo con $F [p]$ una formula proposizionale che può contenere delle occorrenze del simbolo $p$ (detto metavariabile o parametro proposizionale, cioè $p$ sta ad indicare un atomo). Con la notazione $F [X / p]$ indicheremo la formula $F [X]$ , in cui tutte le occorrenze di $p$ sono state uniformemente e simultaneamente sostituite con occorrenze di una formula $X$ . Chiameremo quest'operazione sostituzione uniforme.

Primo teorema del rimpiazzamento

Siano $F [p]$ , $X$ e $Y$ formule proposizionali e sia $I_{𝒱}$ una valutazione booleana. Se $I_{𝒱} (X) = I_{𝒱} (Y)$ , allora

$I_{𝒱} (F [X / p]) = I_{𝒱} (F [Y / p])$ .

Dimostrazione Per induzione strutturale. Osserviamo innanzitutto che, se $p$ non occorre in $F$ , nessuna sostituzione è stata fatta, e quindi l'asserto è banalmente verificato.

(Passo Base) Supponiamo che $F [p] = p$ , allora $F [X / p] = X$ e $F [Y / p] = Y$ ; per ipotesi, $I_{𝒱} (X) = I_{𝒱} (Y)$ , e dunque $I_{𝒱} (F [X / p]) = I_{𝒱} (X) = I_{𝒱} (Y) = I_{𝒱} (F [Y / p])$ .

(Passo Induttivo) Sia $F [p] = \neg A [p]$ . Osserviamo che, per definizione di valutazione booleana:

$I_{𝒱} (F [X / p]) = {𝒪 𝓅}_{\neg} (I_{𝒱} (A [X / p]))$ .

Per ipotesi induttiva: $I_{𝒱} (A [X / p]) = I_{𝒱} (A [Y / p])$ .

Quindi ${𝒪 𝓅}_{\neg} (I_{𝒱} (A [X / p])) = {𝒪 𝓅}_{\neg} (I_{𝒱} (A [Y / p]))$ .

Di nuovo, per definizione di valutazione booleana:

${𝒪 𝓅}_{\neg} (I_{𝒱} (A [Y / p])) = I_{𝒱} (F [Y / p])$ .

Dunque $I_{𝒱} (F [X / p]) = I_{𝒱} (F [Y / p])$ .

Analogamente, sia $F [p] = A [p] \circ B [p]$ , con $\circ \in {\land, \lor, \to, \leftrightarrow}$ . Osserviamo che, per definizione di valutazione booleana:

$I_{𝒱} (F [X / p]) = {𝒪 𝓅}_{\circ} (I_{𝒱} (A [X / p]), I_{𝒱} (B [X / p]))$ .

Per ipotesi induttiva: $I_{𝒱} (A [X / p]) = I_{𝒱} (A [Y / p])$ e $I_{𝒱} (B [X / p]) = I_{𝒱} (B [Y / p])$ .

Quindi ${𝒪 𝓅}_{\circ} (I_{𝒱} (A [X / p]), I_{𝒱} (B [X / p])) = {𝒪 𝓅}_{\circ} (I_{𝒱} (A [Y / p]), I_{𝒱} (B [Y / p]))$ .

Di nuovo, per definizione di valutazione booleana:

${𝒪 𝓅}_{\circ} (I_{𝒱} (A [Y / p]), I_{𝒱} (B [Y / p])) = I_{𝒱} (F [Y / p])$ .

Dunque $I_{𝒱} (F [X / p]) = I_{𝒱} (F [Y / p])$ .

Secondo teorema del rimpiazzamento

Se $X \equiv Y$ , allora $F [X / p] \equiv F [Y / p]$ .

Dimostrazione Essendo $X \equiv Y$ un'equivalenza logica, $I_{𝒱} (X) = I_{𝒱} (Y)$ vale per ogni valutazione booleana $I_{𝒱}$ ; per il primo teorema del rimpiazzamento, si ha che $I_{𝒱} (F [X / p]) = I_{𝒱} (F [Y / p])$ vale per ogni valutazione booleana. Ne consegue che $F [X / p] \equiv F [Y / p]$ .

Modelli

Possiamo fornire una nozione d'interpretazione basata sulla relazione $⊨$ .

Template:Definizione Osserviamo che, nella definizione di $⊨$ , stiamo sottintendendo il linguaggio proposizionale $ℒ$ . Nel caso in cui non sia chiaro dal contesto a quale linguaggio ci si riferisce, allora si usa indicare $⊨_{ℒ}$ .

Modello per una formula

Template:Definizione

Contromodello per una formula

Template:Definizione

Modello per un insieme di formule

Template:Definizione

Se $A$ è una tautologia, possiamo scrivere $⊨ A$ , in quanto $A$ è vera in ogni modello, compreso quello vuoto.

Implicazione logica da un insieme di formule

Template:Definizione

Soddisfacibilità

Template:Definizione

Insoddisfacibilità

Template:DefinizioneQuindi una formula è insoddisfacibile sse per essa non esiste alcun modello.

Il simbolo $⊨$ è giustificato quando si considerano le nozioni di implicazione logica e di equivalenza logica, perché permettono una semplificazione notazionale.

Infatti, se $A$ implica logicamente $B$ scriviamo $⊨ A \to B$ e se $A$ è logicamente equivalente a $B$ , cioè se $A \equiv B$ , scriviamo $⊨ A \leftrightarrow B$ .

Il seguente teorema lega le nozioni di implicazione logica e di insoddisfacibilità:

Teorema di soddisfacibilità

$Γ ⊨ A$ sse $Γ \cup {\neg A}$ è insoddisfacibile.

Dimostrazione

( $\Rightarrow$ ) Supponiamo che valga $Γ ⊨ A$ , ma $Γ \cup {\neg A}$ sia soddisfacibile; allora esiste un modello $ℳ_{𝒱}$ tale che $ℳ_{𝒱} ⊨ Γ$ e $ℳ_{𝒱} ⊨ \neg A$ , cioè $ℳ_{𝒱} ⊨ Γ$ e $ℳ_{𝒱} ⊭ A$ , dunque non vale $Γ ⊨ A$ , contraddizione.

( $\Leftarrow$ ) Supponiamo che $Γ \cup {\neg A}$ sia insoddisfacibile, ma non valga $Γ ⊨ A$ ; allora esiste un modello $ℳ_{𝒱}$ tale che $ℳ_{𝒱} ⊨ Γ$ e $ℳ_{𝒱} ⊭ A$ , cioè $ℳ_{𝒱} ⊨ Γ$ e $ℳ_{𝒱} ⊨ \neg A$ , quindi $ℳ_{𝒱} ⊨ Γ \cup {\neg A}$ , dunque $Γ \cup {\neg A}$ è soddisfacibile, contraddizione.

La proprietà appena enunciata è quella che giustifica le dimostrazioni per assurdo: se si vuole provare che $A$ segue da $Γ$ , basta assumere $\neg A$ e provare che questo contraddice $Γ$ .

Compattezza

Segue quanto abbiamo già notato per le valutazioni booleane: quando consideriamo i modelli di una formula, basta prendere in considerazione solo quelli in cui compaiono i simboli proposizionali della formula. È chiaro che, se in una formula $A$ occorrono $n$ simboli proposizionali distinti, ovvero $| s i m b (A) | = n$ , allora il numero degli insiemi di simboli che ci interessa verificare per conoscere il valore di verità di $A$ è al più $2^{n}$ . Tuttavia, è lecito chiedersi cosa succede se abbiamo un insieme infinito $Γ$ di proposizioni e vogliamo sapere se $Γ ⊨ A$ .

Il teorema di compattezza della soddisfacibilità fornisce una risposta a questa domanda.

Insieme di formule finitamente soddisfacibile

Template:Definizione

Teorema di compattezza della soddisfacibilità

Un insieme di proposizioni $Γ$ è soddisfacibile sse è finitamente soddisfacibile.

Dimostrazione Per contraddizione.

( $\Rightarrow$ ) Supponiamo che $Γ$ sia soddisfacibile, ma che non sia finitamente soddisfacibile. Allora, esiste un sottoinsieme finito $Δ \subseteq Γ$ tale che, per ogni $ℳ_{𝒱}$ , $ℳ_{𝒱} ⊭ A$ , con $A \in Δ$ . Essendo $Δ \subseteq Γ$ , allora $A \in Γ$ , quindi, per ogni $ℳ_{𝒱}$ esiste una formula $A \in Γ$ tale che $ℳ_{𝒱} ⊭ A$ . Dunque, $Γ$ non è soddisfacibile. Contraddizione.

( $\Rightarrow$ ) Supponiamo che $Γ$ sia finitamente soddisfacibile, ma che non sia soddisfacibile. Allora, per ogni $ℳ_{𝒱}$ esiste una formula $A \in Γ$ tale che $ℳ_{𝒱} ⊭ A$ . Quindi, esiste un sottoinsieme finito $Δ \subseteq Γ$ tale che, per ogni $ℳ_{𝒱}$ , $ℳ_{𝒱} ⊭ A$ , con $A \in Δ$ . Perciò, $Δ$ non è soddisfacibile, dunque $Γ$ non è finitamente soddisfacibile. Contraddizione.

Quella qui esposta è una dimostrazione non costruttiva, cioè non fornisce un esempio concreto di ciò che dimostra, ma suppone che la tesi sia falsa e arriva ad una contraddizione. Per una dimostrazione costruttiva, si veda la dimostrazione del teorema di compattezza.

Riformulazione del teorema di compattezza

Il teorema di compattezza può essere enunciato in modo equivalente come segue:

un insieme di proposizioni $Γ$ è insoddisfacibile sse esiste un sottoinsieme finito $Δ \subseteq Γ$ che è insoddisfacibile.

Dimostrazione Per contraddizione.

( $\Rightarrow$ ) Supponiamo che $Γ$ sia insoddisfacibile, ma che non esista un sottoinsieme finito $Δ \subseteq Γ$ insoddisfacibile. Allora, ogni sottoinsieme finito $Δ \subseteq Γ$ è soddisfacibile, quindi $Γ$ è finitamente soddisfacibile. Ma, per il teorema di compattezza, $Γ$ è soddisfacibile. Contraddizione.

( $\Leftarrow$ ) Supponiamo che esista un sottoinsieme finito $Δ \subseteq Γ$ insoddisfacibile, ma che $Γ$ sia soddisfacibile. Allora, per il teorema di compattezza, $Γ$ è finitamente soddisfacibile, quindi ogni sottoinsieme finito $Δ \subseteq Γ$ è soddisfacibile, dunque non può esistere un sottoinsieme finito $Δ \subseteq Γ$ insoddisfacibile. Contraddizione.

Dal teorema di compattezza seguono delle proprietà interessanti, per esempio il seguente corollario.

Corollario del teorema di compattezza

$Γ ⊨ A$ sse esiste un sottoinsieme finito $Γ_{0}$ di $Γ$ tale che $Γ_{0} ⊨ A$ .

Dimostrazione Per contraddizione. Supponiamo che, per ogni $Γ_{0}$ finito, $Γ_{0} ⊭ A$ , e consideriamo le seguenti trasformazioni:

$Γ_{0} ⊭ A$ , per ogni $Γ_{0}$ finito, ipotesi;
sse $Γ_{0} \cup {\neg A}$ è soddisfacibile per ogni $Γ_{0}$ finito (da 1, per il teorema di soddisfacibilità);
sse $Γ \cup {\neg A}$ è finitamente soddisfacibile (da 2, per definizione di insieme finitamente soddisfacibile);
sse $Γ \cup {\neg A}$ è soddisfacibile (da 3, per il teorema di compattezza);
sse $Γ ⊭ A$ (da 4, per il teorema di soddisfacibilità).

Contraddizione.

Teorema di deduzione

Definito il concetto di derivazione semantica, vediamo un importante teorema che permette di ridurre le ipotesi di cui abbiamo bisogno o di sfruttare come ipotesi una parte della sentenza che stiamo analizzando: il teorema di deduzione.

Sia $Γ$ un insieme di formule e siano $A$ e $B$ due formule, allora

Γ, A ⊨ B

sse

Γ ⊨ A \to B

cioè, il teorema dice che $Γ$ e $A$ soddisfano $B$ se e solo se $Γ$ soddisfa $A \to B$ .

Se la cosa può sembrare a prima vista sorprendente, ad una analisi più attenta si può notare come sia la semantica profonda dell'implicazione. Vediamo con un semplice esempio in linguaggio naturale:

da Oggi piove posso derivare ( $⊨$ ) prendo l' ombrello

equivale a:

senza nessuna precondizione posso derivare ( $⊨$ ) se Oggi piove allora ( $\to$ ) prendo l' ombrello

Questo teorema sarà particolarmente utile nelle dimostrazioni, perché ci permette di spostare a destra o a sinistra del simbolo di derivazione l' antecedente dell' implicazione. Quindi, se dobbiamo dimostrare che A implica B, la strada più semplice sarà supporre A come ipotesi e quindi dimostrare B.

Dimostrazione

Per definizione di implicazione logica su un insieme di formule, $Γ, A ⊨ B$ sse, per ogni modello $ℳ_{𝒱}$ , ( $ℳ_{𝒱} ⊭ Γ$ oppure $ℳ_{𝒱} ⊭ A$ oppure $ℳ_{𝒱} ⊨ B$ ).

Per definizione di $⊨$ , ( $ℳ_{𝒱} ⊭ A$ oppure $ℳ_{𝒱} ⊨ B$ ) sse ( $I_{𝒱} (A) = F$ oppure $I_{𝒱} (B) = T$ ) sse ${𝒪 𝓅}_{\lor} ({𝒪 𝓅}_{\neg} (I_{𝒱} (A)), I_{𝒱} (B)) = T$ . Per definizione di ${𝒪 𝓅}_{\to}$ , ${𝒪 𝓅}_{\lor} ({𝒪 𝓅}_{\neg} (I_{𝒱} (A)), I_{𝒱} (B)) = {𝒪 𝓅}_{\to} (I_{𝒱} (A), I_{𝒱} (B)) = I_{𝒱} (A \to B) = T$ . Per definizione di $⊨$ , $I_{𝒱} (A \to B) = T$ sse $ℳ_{𝒱} ⊨ A \to B$ . Dunque, $Γ, A ⊨ B$ sse ( $ℳ_{𝒱} ⊭ Γ$ oppure $ℳ_{𝒱} ⊨ A \to B$ ) sse $Γ ⊨ A \to B$ .

Completezza di insiemi di connettivi

I connettivi definiscono delle funzioni da $ℬ$ (nel caso del connettivo unario $\neg$ ), oppure $ℬ \times ℬ$ (nel caso dei connettivi binari) in $ℬ$ . Ciascuna di queste funzioni, dette funzioni booleane, è definita attraverso la relativa tavola dei valori di verità, oppure, equivalentemente, attraverso le funzioni ${𝒪 𝓅}_{\neg}$ e ${𝒪 𝓅}_{\circ}$ , con $\circ \in {\land, \lor, \to, \leftrightarrow}$ .

Più in generale, ogni formula proposizionale $A$ contenente simboli proposizionali distinti $A_{1}, . . ., A_{n}$ definisce una funzione booleana da $ℬ^{n}$ in $ℬ$ .

Funzione di verità

Template:Definizione

Quindi, ogni formula del calcolo proposizionale definisce una funzione $n$ -aria (possiamo anche chiamarla connettivo $n$ -ario), dove $n$ è il numero di atomi distinti che in essa compaiono. Si può facilmente verificare che, per ogni $n$ , esistono $2^{2^{n}}$ funzioni booleane distinte (cioè, tante quanti sono i sottoinsiemi di $ℬ^{n}$ ). Quindi, nel caso di $n = 2$ esistono 16 connettivi distinti. Qui ne sono stati introdotti 4 e, come alcune equivalenze logiche introdotte precedentemente hanno mostrato, essi non sono indipendenti, nel senso che alcuni sono esprimibili in termini di altri.

Derivazione di connettivi

Template:Definizione

Nella logica proposizionale valgono le seguenti equivalenze logiche.

$A \to B$	$\equiv$	$\neg A \lor B$
$A \lor B$	$\equiv$	$\neg A \to B$
$A \lor B$	$\equiv$	$\neg (\neg A \land \neg B)$
$A \land B$	$\equiv$	$\neg (\neg A \lor \neg B)$
$A \land B$	$\equiv$	$(((A \to ⊥) \to ⊥) \to (B \to ⊥)) \to ⊥$
$\neg A$	$\equiv$	$A \to ⊥$
$⊥$	$\equiv$	$A \land \neg A$
$A \leftrightarrow B$	$\equiv$	$(A \to B) \land (B \to A)$

Si noti che la costante proposizionale $⊥$ (così come la costante proposizionale $⊤$ ) può essere considerata come un connettivo $0$ -ario.

Un insieme di connettivi logici è completo se mediante i suoi connettivi si può esprimere qualunque funzione booleana. Più formalmente diciamo che:

Insieme funzionalmente completo

Template:Vedi anche Template:Definizione

In particolare, un insieme di connettivi logici è completo se mediante i suoi connettivi si può esprimere qualunque altro connettivo.

È facile verificare che l'insieme dei connettivi ${\neg, \land, \lor}$ è completo, così come lo sono ${\neg, \land}$ e anche ${\neg, \lor}$ .

Questo ci porta a concludere che nella trattazione della logica potremmo ridurci a considerare due soli connettivi. Si può in effetti anche dimostrare che un solo connettivo binario può bastare per definire tutti gli altri; in particolare, un connettivo a scelta tra il "nand" o il "nor" costituisce un insieme completo. Si può anche dimostrare che nand e nor sono gli unici due connettivi binari completi.

Usare un minor numero di connettivi nelle formule porterebbe sicuramente a una maggiore stringatezza nelle dimostrazioni date per casi sui singoli connettivi, ma nuocerebbe gravemente alla leggibilità delle formule stesse. Le equivalenze sopra mostrate ne forniscono evidenza. Si è quindi preferito la leggibilità alla concisione.

Decidibilità

La logica proposizionale è decidibile. In effetti, la logica proposizionale si chiama calcolo delle proposizioni perché esiste una procedura effettiva che stabilisce se una proposizione $A$ è una tautologia o meno. Nel caso del calcolo proposizionale, possiamo sempre essere in grado di calcolare le formule vere del linguaggio. In verità, come si vedrà nel caso della logica del primo ordine, la dizione calcolo si usa anche qualora si abbia una logica semidecidibile.

Per verificare la decidibilità del calcolo proposizionale siamo interessati a decidere se una formula $A$ del calcolo proposizionale è una tautologia o meno.

Un altro interessante problema di decisione per il calcolo proposizionale consiste nello stabilire se una formula è soddisfacibile o meno (questo problema è di solito indicato con SAT).

Abbiamo visto che, per decidere se $A$ è una tautologia, bisogna verificare le tavole di verità per ogni assegnazione ai simboli proposizionali che occorrono in $A$ ; pertanto, se in $A$ occorrono $n$ simboli proposizionali, sarà sufficiente verificare $2^{n}$ casi.

Diciamo che un insieme $Γ$ di formule è enumerabile se può essere trasformato in una sequenza. Un insieme di formule è effettivamente enumerabile se esiste un metodo per determinare l' $n$ -esimo elemento della sequenza, per ogni $n \in ℕ$ .

Lemma di enumerabilità

Se $Γ$ è effettivamente enumerabile, allora l'insieme delle conseguenze tautologiche di $Γ$ , ovvero l'insieme ${A | Γ ⊨ A}$ è effettivamente enumerabile.

Dimostrazione

Dobbiamo mostrare che, data una formula $A$ , se $Γ ⊨ A$ , allora esiste una procedura che risponde SÌ. Consideriamo un'enumerazione $Γ_{0}, Γ_{1}, Γ_{2}, . . .$ dei sottoinsiemi finiti di $Γ$ . Data una formula $A$ , consideriamo la lista dei sottoinsiemi finiti di $Γ$ nel seguente modo:

$⊨ A,$

$Γ_{0} ⊨ A,$

$Γ_{1} ⊨ A,$

$. . .$

Per il corollario del teorema di compattezza, se $Γ ⊨ A$ esiste un $Γ_{i}$ finito tale che $Γ_{i} ⊨ A$ , e dunque tale $Γ_{i}$ comparirà nell'enumerazione.

Teoria della dimostrazione

Come abbiamo visto nel paragrafo precedente, il calcolo delle proposizioni è decidibile ed abbiamo un algoritmo (le tavole di verità) per verificare se una sentenza è soddisfacibile. Ora cercheremo dei metodi che ci permettano di dimostrare che una sentenza è valida.

Il metodo delle tabelle di verità è un metodo "semantico", cioè che esplora tutte le possibili configurazioni dell'universo per verificarne lo stato, ora vogliamo costruire dei metodi basati più sulla deduzione che non sull'esplorazione e che si basino sull'attività di costruire derivazioni e dimostrazioni, cioè sul ragionamento e non sulla forza bruta.

Svilupperemo quindi dei metodi puramente sintattici, cioè dei calcoli che trasformano simboli in altri simboli, che ci permetteranno di creare dimostrazioni sulle sentenze logiche.

Introduciamo un nuovo simbolo $⊢$ , per indicare che da una sentenza possiamo derivare sintatticamente un'altra sentenza.

Abbiamo così due concetti:

$A ⊨ B$

significa che semanticamente se $A$ è vera anche $B$ è vera, mentre

$A ⊢ B$

significa che se $A$ è vera possiamo costruire una dimostrazione di $B$ .

Il grande risultato della logica moderna è stato legare tra loro questi due concetti nel teorema di completezza, che vedremo più avanti.

Esploreremo i maggiori sistemi di dimostrazione, tutti con peculiari caratteristiche. Il sistema di Hilbert è quello più simile alla definizione del metodo assiomatico, i sistemi di Gentzen (deduzione naturale e sequenti) tentano di mimare l'attività mentale di un matematico, i tableaux sfruttano la semantica e la risoluzione è il sistema più semplice da realizzare meccanicamente, tanto da essere alla base del linguaggio di programmazione PROLOG.

Il sistema di Hilbert si basa su un insieme di assiomi logici e un insieme di regole di inferenza; i tableaux e la risoluzione invece non fanno uso di assiomi logici, ma solo di regole di inferenza e sono basati sulla refutazione (cioè, per dimostrare che una formula è un teorema si dimostra in effetti che la sua negata è una contraddizione). Tra questi metodi, solo la risoluzione richiede che le formule siano scritte in una forma normale.

Tutti i sistemi deduttivi presentati sono per certi aspetti equivalenti, per tutti infatti vale un teorema di correttezza e completezza, quindi l'insieme di teoremi che si può derivare con ciascuno di essi è lo stesso.

Correttezza e completezza di un sistema

Ogni sistema di dimostrazione, per essere un buon sistema, deve avere due proprietà: essere corretto ed essere completo.

La proprietà di correttezza è:

se $⊢_{s} Φ$ allora $⊨ Φ$ .

cioè, se posso dimostrare $Φ$ con il sistema $S$ , allora $Φ$ è una tautologia. In poche parole, tutto quello che può essere provato da $S$ è vero.

La proprietà di completezza è:

se $⊨ Φ$ allora $⊢_{s} Φ$ .

cioè, se una proposizione è una tautologia, posso dimostrarla utilizzando $S$ .

I principali sistemi di dimostrazione

Template:Avanzamento

Logica matematica/Calcolo delle proposizioni

Sintassi

Alfabeto

Formule ben formate

Sottoformule

Simboli proposizionali occorrenti in una formula

Esempi

Semantica

Sistema di valutazione

Negazione

Congiunzione

Disgiunzione

Implicazione

Doppia implicazione

Assegnazione booleana

Valutazione booleana

Teorema di equivalenza delle valutazioni

Soddisfacibilità

Formula soddisfatta

Formula soddisfacibile

Tautologia

Contraddizione

Tavole di verità

Teorema

Equivalenza logica

Implicazione logica

Equivalenza logica (Definizione)

Primo teorema del rimpiazzamento

Secondo teorema del rimpiazzamento

Modelli

Modello per una formula

Contromodello per una formula

Modello per un insieme di formule

Implicazione logica da un insieme di formule

Soddisfacibilità

Insoddisfacibilità

Teorema di soddisfacibilità

Compattezza

Insieme di formule finitamente soddisfacibile

Teorema di compattezza della soddisfacibilità

Riformulazione del teorema di compattezza

Corollario del teorema di compattezza

Teorema di deduzione

Dimostrazione

Completezza di insiemi di connettivi

Funzione di verità

Derivazione di connettivi

Insieme funzionalmente completo

Decidibilità

Lemma di enumerabilità

Dimostrazione

Teoria della dimostrazione

Correttezza e completezza di un sistema

I principali sistemi di dimostrazione

Menu di navigazione

Ricerca