Logica matematica/Calcolo delle proposizioni

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 ${\mathcal {L}}_{\Sigma }$ costruito su un alfabeto $\Sigma$. Iniziamo con la definizione di alfabeto.

Alfabeto

Definizione

Un alfabeto $\Sigma$ è costituito da:

• i connettivi proposizionali $\neg$ (unario) e $\land ,\lor ,\to ,\leftrightarrow$ (binari);
• le costanti proposizionali $\top ,\bot$ (per denotare il vero e il falso);
• un insieme non vuoto (finito o numerabile) di simboli proposizionali ${\mathcal {P}}=\{A,B,C,...\}$;
• i simboli separatori $'('$ e $')'$.

Nel seguito scriveremo ${\mathcal {L}}$ quando $\Sigma$ è chiaro dal contesto. Definiamo ora le formule di ${\mathcal {L}}$.

Formule ben formate

Definizione

L'insieme PROP delle formule ben formate o formule del linguaggio proposizionale ${\mathcal {L}}$ è l'insieme definito induttivamente come segue:

1. le costanti e i simboli proposizionali sono formule;
2. se $A$ è una formula, $(\neg A)$ è una formula;
3. se $\circ$ è un connettivo binario (cioè $\circ \in \{\land ,\lor ,\to ,\leftrightarrow \}$) e se $A$ e $B$ sono due formule, $(A\circ B)$ è una formula.

Le costanti e i simboli proposizionali sono anche detti atomi, le loro negazioni sono dette atomi negati. Gli atomi e gli atomi negati sono anche detti letterali. Gli atomi negati sono talvolta detti letterali negativi. Una formula del linguaggio proposizionale è anche detta proposizione o enunciato proposizionale.

Data una formula $A$ di PROP, ogni formula $B$ che appare come componente di $A$ è detta sottoformula di $A$. La definizione di sottoformula, di connettivo principale e di sottoformula immediata è la seguente.

Sottoformule

Definizione

Sia $A$ una formula di PROP, l'insieme delle sottoformule di $A$ è definito come segue:

1. $A$ stessa è una sottoformula di $A$;
2. se $A$ è una formula del tipo $(\neg B)$, allora le sottoformule di $B$ sono anche sottoformule di $A$; $\neg$ è detto connettivo principale e $B$ sottoformula immediata di $A$;
3. se $A$ è una formula del tipo $B\circ C$, dove $\circ$ è un connettivo binario (cioè $\circ \in \{\lor ,\land ,\rightarrow ,\leftrightarrow \}$), e $B$ e $C$ due formule, le sottoformule di $B$ e $C$ sono anche sottoformule di $A$; $\circ$ è detto connettivo principale; $B$ e $C$ sottoformule immediate di $A$.

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

Definizione

La funzione

$simb:\mathrm {PROP} \mapsto \wp {\mathcal {P}}$

su PROP nell'inseme potenza di ${\mathcal {P}}$ è definita ricorsivamente come segue:

• $simb(A)=\{A\}$ se $A\in {\mathcal {P}}$;
• $simb(\top )=\emptyset$;
• $simb(\bot )=\emptyset$;
• $simb(\neg A)=simb(A)$;
• $simb(A\circ B)=simb(A)\cup simb(B)$, dove $\circ \in \{\land ,\lor ,\to ,\leftrightarrow \}$.

La funzione $simb$ restituisce l'insieme dei simboli proposizionali che occorrono in una formula. Essa è definita in $\wp {\mathcal {P}}$, cioè nell'inseme dei sottoinsiemi di ${\mathcal {P}}$, dato che restituisce sempre un sottoinsieme di ${\mathcal {P}}$.

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:

1. $((A\to B)\land (C\to D))\to ((A\land C)\to (B\land D))$
2. $\neg A\to \neg \neg \neg A$
3. $A\leftrightarrow B\lor C$

mentre frasi invalide sono:

1. $A(B)$
2. $\to A\to B$
3. $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

Per approfondire, vedi Tutti i connettivi.

Definizione

Il sistema di valutazione ${\mathcal {S}}=\langle {\mathcal {B}},{\mathcal {T}},{\mathcal {Op}}\rangle$ della logica proposizionale è definito da

1. ${\displaystyle {\mathcal {B}}=\{\mathrm {T} ,\mathrm {F} \}}$
2. ${\mathcal {T}}=\{\mathrm {T} \}$;
3. ${\mathcal {Op}}=\{{\mathcal {Op}}_{\neg },{\mathcal {Op}}_{\land },{\mathcal {Op}}_{\lor },{\mathcal {Op}}_{\to },{\mathcal {Op}}_{\leftrightarrow }\}$, uno per ognuno dei connettivi del linguaggio $\{\neg ,\land ,\lor ,\rightarrow ,\leftrightarrow \}$, con:
   • ${\mathcal {Op}}_{\neg }:{\mathcal {B}}\mapsto {\mathcal {B}}$;
   • ${\mathcal {Op}}_{\circ }:{\mathcal {B}}\times {\mathcal {B}}\mapsto {\mathcal {B}}$, $\circ \in \{\land ,\lor ,\to ,\leftrightarrow \}$.

Negazione

Definizione

La funzione ${\mathcal {Op}}_{\neg }$ della logica proposizionale è definita come segue:

• ${\mathcal {Op}}_{\neg }(\mathrm {T} )=\mathrm {F}$
• ${\mathcal {Op}}_{\neg }(\mathrm {F} )=\mathrm {T}$

Questo è di solito espresso in maniera concisa come:

• $\neg (\mathrm {T} )=\mathrm {F}$
• $\neg (\mathrm {F} )=\mathrm {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{array}{|c|c|}A&\neg A\\\hline \mathrm {F} &\mathrm {T} \\\mathrm {T} &\mathrm {F} \end{array}}$

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 ${\mathcal {Op}}_{\circ }$ della logica proposizionale per i connettivi binari, le presentiamo subito in forma di tabella dei valori di verità.

Congiunzione

Definizione

${\begin{array}{|c|c|c|}A&B&A\land B\\\hline \mathrm {F} &\mathrm {F} &\mathrm {F} \\\mathrm {F} &\mathrm {T} &\mathrm {F} \\\mathrm {T} &\mathrm {F} &\mathrm {F} \\\mathrm {T} &\mathrm {T} &\mathrm {T} \\\end{array}}$

Il connettivo di congiunzione $\land$ viene definito in modo che $A\land B$ è vero se sia $A$ che $B$ (i due congiunti) sono veri, quindi ${\mathcal {Op}}_{\land }=min$.

Disgiunzione

Definizione

${\begin{array}{|c|c|c|}A&B&A\lor B\\\hline \mathrm {F} &\mathrm {F} &\mathrm {F} \\\mathrm {F} &\mathrm {T} &\mathrm {T} \\\mathrm {T} &\mathrm {F} &\mathrm {T} \\\mathrm {T} &\mathrm {T} &\mathrm {T} \\\end{array}}$

Il connettivo di disgiunzione $\lor$ viene definito in modo che $A\lor B$ è vero se $A$ oppure $B$ (uno dei due disgiunti) sono veri, quindi ${\mathcal {Op}}_{\lor }=max$. Si noti che, con questa definizione, $\lor$ è la disgiunzione inclusiva, cioè corrisponde al "vel" latino e non all'"aut".

Implicazione

Definizione

${\mathcal {Op}}_{\to }(A,B)={\mathcal {Op}}_{\lor }({\mathcal {Op}}_{\neg }(A),B)$

La definizione della semantica del connettivo di implicazione $A\to B$ (detta implicazione materiale, in cui $A$ è detto premessa e $B$ conseguenza) è, in un certo senso, meno intuitiva. Innanzi tutto si noti che, con la definizione data, si ha che $A\to A$ è sempre vero, qualunque sia il valore di verità di $A$; questo corrisponde alla nostra intuizione. Possiamo quindi accettare il fatto che, affinché $A\to B$ sia vero, basta che $B$ sia vero, indipendentemente dal valore di verità di $A$. Questo di fatto ci dice che, se $B$ è vero e $B\to B$ è vero, possiamo "rafforzare" la premessa sostituendo a $B$ un qualunque $A$ e l'implicazione resta vera. In sostanza, l'implicazione è falsa nel solo caso in cui la premessa è vera e la conseguenza è falsa.

Doppia implicazione

Definizione

${\begin{array}{|c|c|c|}A&B&A\leftrightarrow B\\\hline \mathrm {F} &\mathrm {F} &\mathrm {T} \\\mathrm {F} &\mathrm {T} &\mathrm {F} \\\mathrm {T} &\mathrm {F} &\mathrm {F} \\\mathrm {T} &\mathrm {T} &\mathrm {T} \\\end{array}}$

La definizione della semantica del connettivo di doppia implicazione è del tutto intuitiva: il valore di verità di $A\leftrightarrow B$ è vero se i valori di verità di $A$ e $B$ coincidono.

Assegnazione booleana

Definizione

Un'assegnazione booleana ${\mathcal {V}}$ ai simboli proposizionali ${\mathcal {P}}$ è una funzione totale

${\mathcal {V}}:{\mathcal {P}}\mapsto {\mathcal {B}}$

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

Valutazione booleana

Definizione

Una valutazione booleana

$I_{\mathcal {V}}:\mathrm {PROP} \mapsto {\mathcal {B}}$

è l'estensione a PROP di un'assegnazione booleana, cioè

• $I_{\mathcal {V}}(A)={\mathcal {V}}(A)$ se $A\in {\mathcal {P}}$;
• $I_{\mathcal {V}}(\top )=\mathrm {T}$;
• $I_{\mathcal {V}}(\bot )=\mathrm {F}$;
• $I_{\mathcal {V}}(\neg A)={\mathcal {Op}}_{\neg }(I_{\mathcal {V}}(A))$;
• $I_{\mathcal {V}}(A\circ B)={\mathcal {Op}}_{\circ }(I_{\mathcal {V}}(A),I_{\mathcal {V}}(B))$.

dove $\circ \in \{\land ,\lor ,\to ,\leftrightarrow \}$. Data un'assegnazione booleana ${\mathcal {V}}$, l'esistenza e l'unicità dell'estensione $I_{\mathcal {V}}$ sono garantite dal teorema di ricorsione.

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 $simb(A)$ l'insieme dei simboli proposizionali che occorrono in $A$, per essi vale la seguente proprietà.

Teorema di equivalenza delle valutazioni

Se ${\mathcal {V}}_{1}$ e ${\mathcal {V}}_{2}$ sono due assegnazioni che coincidono su $simb(A)$, allora $I_{\mathcal {V_{1}}}(A)=I_{\mathcal {V_{2}}}(A)$.

Dimostrazione Procediamo per induzione strutturale.

• (Passo Base) Osserviamo che l'asserto è vero per le formule $\bot$ e $\top$ perché non contengono simboli proposizionali. Se $A\in {\mathcal {P}}$, allora abbiamo ${\mathcal {V_{1}}}(A)={\mathcal {V_{2}}}(A)$ e, per definizione, $I_{\mathcal {V_{1}}}(A)=I_{\mathcal {V_{2}}}(A)$. Pertanto l'asserto vale per i simboli proposizionali.

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

Soddisfacibilità

Formula soddisfatta

Definizione

Una formula della logica proposizionale $A$ è soddisfatta da una valutazione booleana $I_{\mathcal {V}}$ sse $I_{\mathcal {V}}(A)=\mathrm {T}$.

Formula soddisfacibile

Definizione

Una formula della logica proposizionale $A$ è soddisfacibile sse è soddisfatta da una qualche valutazione booleana $I_{\mathcal {V}}$.

Tautologia

Definizione

Una formula della logica proposizionale $A$ è tautologica, ossia è una tautologia, sse è soddisfatta da ogni valutazione booleana $I_{\mathcal {V}}$.

Contraddizione

Definizione

Una formula della logica proposizionale $A$ è contraddittoria, ossia è una contraddizione, sse non è soddisfatta da alcuna valutazione booleana $I_{\mathcal {V}}$.

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_{\mathcal {V}}(A)$. La tabella ha $2^{n}$ righe, tante quante sono le possibili assegnazioni distinte di valori di verità ai simboli di $A$.

${\begin{array}{|c|c|c|c|}A_{1}&...&A_{n}&I_{\mathcal {V}}(A)\\\hline \mathrm {F} &...&\mathrm {F} &I_{\mathcal {V_{1}}}(A)\\...&...&...&...\\\mathrm {T} &...&\mathrm {T} &I_{\mathcal {V_{2^{n}}}}(A)\\\end{array}}$

$A$ è una tautologia sse l'ultima colonna contiene solo $\mathrm {T}$, è soddisfacibile sse essa contiene almeno una $\mathrm {T}$, è contraddittoria sse essa contiene tutte $\mathrm {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_{\mathcal {V}}$ si ha che $I_{\mathcal {V}}(A)=\mathrm {T}$. Ora, per $\neg A$ si ha che:

$I_{\mathcal {V}}(\neg A)={\mathcal {Op}}_{\neg }(I_{\mathcal {V}}(A))={\mathcal {Op}}_{\neg }(\mathrm {T} )=\mathrm {F}$

quindi, per ogni valutazione booleana $I_{\mathcal {V}}$ si ha che:

$I_{\mathcal {V}}(\neg A)=\mathrm {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_{\mathcal {V}}$ si ha che $I_{\mathcal {V}}(\neg A)=\mathrm {F}$. Ora, per $\neg A$ si ha che:

$I_{\mathcal {V}}(\neg A)={\mathcal {Op}}_{\neg }(I_{\mathcal {V}}(A))$

quindi:

${\mathcal {Op}}_{\neg }(I_{\mathcal {V}}(A))=\mathrm {F}$

da cui, per la definizione di ${\mathcal {Op}}_{\neg }$, si deduce che, per ogni valutazione booleana $I_{\mathcal {V}}$:

$I_{\mathcal {V}}(A)=\mathrm {T}$

dunque, $A$ è una tautologia.

Equivalenza logica

Implicazione logica

Definizione

Diciamo che $A$ implica logicamente $B$ sse ogniqualvolta $I_{\mathcal {V}}(A)=\mathrm {T}$ anche $I_{\mathcal {V}}(B)=\mathrm {T}$.

Equivalenza logica (Definizione)

Definizione

Diciamo che due proposizioni $A$ e $B$ sono logicamente equivalenti o tautologicamente equivalenti sse $I_{\mathcal {V}}(A)=I_{\mathcal {V}}(B)$ per ogni valutazione booleana $I_{\mathcal {V}}$. In tal caso scriviamo $A\equiv B$.

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 \top$	$\equiv$	$A$	neutralità del vero nella congiunzione
$A\lor \top$	$\equiv$	$\top$	assorbimento del vero nella disgiunzione
$A\lor \bot$	$\equiv$	$A$	neutralità del falso nella disgiunzione
$A\land \bot$	$\equiv$	$\bot$	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$	$\top$	terzo escluso
$A\land \neg A$	$\equiv$	$\bot$	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_{\mathcal {V}}$ una valutazione booleana. Se $I_{\mathcal {V}}(X)=I_{\mathcal {V}}(Y)$, allora

$I_{\mathcal {V}}(F[X/p])=I_{\mathcal {V}}(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_{\mathcal {V}}(X)=I_{\mathcal {V}}(Y)$, e dunque $I_{\mathcal {V}}(F[X/p])=I_{\mathcal {V}}(X)=I_{\mathcal {V}}(Y)=I_{\mathcal {V}}(F[Y/p])$.

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

$I_{\mathcal {V}}(F[X/p])={\mathcal {Op}}_{\neg }(I_{\mathcal {V}}(A[X/p]))$.

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

Quindi ${\mathcal {Op}}_{\neg }(I_{\mathcal {V}}(A[X/p]))={\mathcal {Op}}_{\neg }(I_{\mathcal {V}}(A[Y/p]))$.

Di nuovo, per definizione di valutazione booleana:

${\mathcal {Op}}_{\neg }(I_{\mathcal {V}}(A[Y/p]))=I_{\mathcal {V}}(F[Y/p])$.

Dunque $I_{\mathcal {V}}(F[X/p])=I_{\mathcal {V}}(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_{\mathcal {V}}(F[X/p])={\mathcal {Op}}_{\circ }(I_{\mathcal {V}}(A[X/p]),I_{\mathcal {V}}(B[X/p]))$.

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

Quindi ${\mathcal {Op}}_{\circ }(I_{\mathcal {V}}(A[X/p]),I_{\mathcal {V}}(B[X/p]))={\mathcal {Op}}_{\circ }(I_{\mathcal {V}}(A[Y/p]),I_{\mathcal {V}}(B[Y/p]))$.

Di nuovo, per definizione di valutazione booleana:

${\mathcal {Op}}_{\circ }(I_{\mathcal {V}}(A[Y/p]),I_{\mathcal {V}}(B[Y/p]))=I_{\mathcal {V}}(F[Y/p])$.

Dunque $I_{\mathcal {V}}(F[X/p])=I_{\mathcal {V}}(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_{\mathcal {V}}(X)=I_{\mathcal {V}}(Y)$ vale per ogni valutazione booleana $I_{\mathcal {V}}$; per il primo teorema del rimpiazzamento, si ha che $I_{\mathcal {V}}(F[X/p])=I_{\mathcal {V}}(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 $\models$.

Definizione

Sia ${\mathcal {V}}$ un'assegnazione booleana. L'insieme ${\mathcal {M_{V}}}$ associato a ${\mathcal {V}}$ è l'insieme dei simboli proposizionali tali che il loro valore di verità in ${\mathcal {V}}$ sia $\mathrm {T}$. Più formalmente:

${\mathcal {M_{V}}}=\{p|p\in {\mathcal {P}},{\mathcal {V}}(p)=\mathrm {T} \}$

Definiamo la relazione $\models \subseteq (\wp {\mathcal {P}}\times {\mathcal {L}})$ come segue:

${\mathcal {M_{V}}}\models A$ sse $I_{\mathcal {V}}(A)=\mathrm {T}$

${\mathcal {M_{V}}}\nvDash A$ sse $I_{\mathcal {V}}(A)=\mathrm {F}$

Osserviamo che, nella definizione di $\models$, stiamo sottintendendo il linguaggio proposizionale ${\mathcal {L}}$. Nel caso in cui non sia chiaro dal contesto a quale linguaggio ci si riferisce, allora si usa indicare $\models _{\mathcal {L}}$.

Modello per una formula

Definizione

Sia $A$ una formula. Se ${\mathcal {M_{V}}}\models A$ diciamo che ${\mathcal {M_{V}}}$ è un modello di $A$, ovvero che ${\mathcal {M_{V}}}$ rende vera $A$.

Contromodello per una formula

Definizione

Sia $A$ una formula. Se ${\mathcal {M_{V}}}\nvDash A$ diciamo che ${\mathcal {M_{V}}}$ è un contromodello per $A$, ovvero che ${\mathcal {M_{V}}}$ rende falsa $A$.

Modello per un insieme di formule

Definizione

Se ${\mathcal {M_{V}}}$ rende vere tutte le formule di un insieme $\Gamma$, cioè se ${\mathcal {M_{V}}}\models A$ per ogni formula $A$ in $\Gamma$, diciamo che ${\mathcal {M_{V}}}$ è un modello per $\Gamma$ e indichiamo ciò con ${\mathcal {M_{V}}}\models \Gamma$.

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

Implicazione logica da un insieme di formule

Definizione

Dato un insieme di formule $\Gamma$ e una formula $A$, diciamo che $\Gamma$ soddisfa $A$, o implica logicamente $A$, e scriviamo $\Gamma \models A$, sse (${\mathcal {M_{V}}}\nvDash \Gamma$ oppure ${\mathcal {M_{V}}}\models A$).

Soddisfacibilità

Definizione

Se ${\mathcal {M_{V}}}\models A$ per qualche ${\mathcal {M_{V}}}$, allora diciamo che $A$ è soddisfacibile.

Insoddisfacibilità

Definizione

Se per nessun insieme di simboli proposizionali ${\mathcal {M_{V}}}$ è verificato che ${\mathcal {M_{V}}}\models A$, allora diciamo che $A$ è insoddisfacibile.

Quindi una formula è insoddisfacibile sse per essa non esiste alcun modello.

Il simbolo $\models$ è 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 $\vDash A\to B$ e se $A$ è logicamente equivalente a $B$, cioè se $A\equiv B$, scriviamo $\vDash A\leftrightarrow B$.

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

Teorema di soddisfacibilità

$\Gamma \models A$ sse $\Gamma \cup \{\neg A\}$ è insoddisfacibile.

Dimostrazione

($\Rightarrow$) Supponiamo che valga $\Gamma \models A$, ma $\Gamma \cup \{\neg A\}$ sia soddisfacibile; allora esiste un modello ${\mathcal {M_{V}}}$ tale che ${\mathcal {M_{V}}}\models \Gamma$ e ${\mathcal {M_{V}}}\models \neg A$, cioè ${\mathcal {M_{V}}}\models \Gamma$ e ${\mathcal {M_{V}}}\nvDash A$, dunque non vale $\Gamma \models A$, contraddizione.

($\Leftarrow$) Supponiamo che $\Gamma \cup \{\neg A\}$ sia insoddisfacibile, ma non valga $\Gamma \models A$; allora esiste un modello ${\mathcal {M_{V}}}$ tale che ${\mathcal {M_{V}}}\models \Gamma$ e ${\mathcal {M_{V}}}\nvDash A$, cioè ${\mathcal {M_{V}}}\models \Gamma$ e ${\mathcal {M_{V}}}\models \neg A$, quindi ${\mathcal {M_{V}}}\models \Gamma \cup \{\neg A\}$, dunque $\Gamma \cup \{\neg A\}$ è soddisfacibile, contraddizione.

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

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 $|simb(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 $\Gamma$ di proposizioni e vogliamo sapere se $\Gamma \models A$.

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

Insieme di formule finitamente soddisfacibile

Definizione

Un insieme di formule $\Gamma$ si dice finitamente soddisfacibile sse ogni suo sottoinsieme finito è soddisfacibile.

Teorema di compattezza della soddisfacibilità

Un insieme di proposizioni $\Gamma$ è soddisfacibile sse è finitamente soddisfacibile.

Dimostrazione Per contraddizione.

($\Rightarrow$) Supponiamo che $\Gamma$ sia soddisfacibile, ma che non sia finitamente soddisfacibile. Allora, esiste un sottoinsieme finito $\Delta \subseteq \Gamma$ tale che, per ogni ${\mathcal {M_{V}}}$, ${\mathcal {M_{V}}}\nvDash A$, con $A\in \Delta$. Essendo $\Delta \subseteq \Gamma$, allora $A\in \Gamma$, quindi, per ogni ${\mathcal {M_{V}}}$ esiste una formula $A\in \Gamma$ tale che ${\mathcal {M_{V}}}\nvDash A$. Dunque, $\Gamma$ non è soddisfacibile. Contraddizione.

($\Rightarrow$) Supponiamo che $\Gamma$ sia finitamente soddisfacibile, ma che non sia soddisfacibile. Allora, per ogni ${\mathcal {M_{V}}}$ esiste una formula $A\in \Gamma$ tale che ${\mathcal {M_{V}}}\nvDash A$. Quindi, esiste un sottoinsieme finito $\Delta \subseteq \Gamma$ tale che, per ogni ${\mathcal {M_{V}}}$, ${\mathcal {M_{V}}}\nvDash A$, con $A\in \Delta$. Perciò, $\Delta$ non è soddisfacibile, dunque $\Gamma$ 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 $\Gamma$ è insoddisfacibile sse esiste un sottoinsieme finito $\Delta \subseteq \Gamma$ che è insoddisfacibile.

Dimostrazione Per contraddizione.

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

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

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

Corollario del teorema di compattezza

$\Gamma \models A$ sse esiste un sottoinsieme finito $\Gamma _{0}$ di $\Gamma$ tale che $\Gamma _{0}\models A$.

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

1. $\Gamma _{0}\nvDash A$, per ogni $\Gamma _{0}$ finito, ipotesi;
2. sse $\Gamma _{0}\cup \{\neg A\}$ è soddisfacibile per ogni $\Gamma _{0}$ finito (da 1, per il teorema di soddisfacibilità);
3. sse $\Gamma \cup \{\neg A\}$ è finitamente soddisfacibile (da 2, per definizione di insieme finitamente soddisfacibile);
4. sse $\Gamma \cup \{\neg A\}$ è soddisfacibile (da 3, per il teorema di compattezza);
5. sse $\Gamma \nvDash 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 $\Gamma$ un insieme di formule e siano $A$ e $B$ due formule, allora

$\Gamma ,A\models B$ sse $\Gamma \models A\to B$

cioè, il teorema dice che $\Gamma$ e $A$ soddisfano $B$ se e solo se $\Gamma$ 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 ($\models$) prendo l' ombrello

equivale a:

senza nessuna precondizione posso derivare ($\models$) 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, $\Gamma ,A\models B$ sse, per ogni modello ${\mathcal {M_{V}}}$, (${\mathcal {M_{V}}}\nvDash \Gamma$ oppure ${\mathcal {M_{V}}}\nvDash A$ oppure ${\mathcal {M_{V}}}\models B$).

Per definizione di $\models$, (${\mathcal {M_{V}}}\nvDash A$ oppure ${\mathcal {M_{V}}}\models B$) sse ($I_{\mathcal {V}}(A)=\mathrm {F}$ oppure $I_{\mathcal {V}}(B)=\mathrm {T}$) sse ${\mathcal {Op}}_{\lor }({\mathcal {Op}}_{\neg }(I_{\mathcal {V}}(A)),I_{\mathcal {V}}(B))=\mathrm {T}$. Per definizione di ${\mathcal {Op}}_{\to }$, ${\mathcal {Op}}_{\lor }({\mathcal {Op}}_{\neg }(I_{\mathcal {V}}(A)),I_{\mathcal {V}}(B))={\mathcal {Op}}_{\to }(I_{\mathcal {V}}(A),I_{\mathcal {V}}(B))=I_{\mathcal {V}}(A\to B)=\mathrm {T}$. Per definizione di $\models$, $I_{\mathcal {V}}(A\to B)=\mathrm {T}$ sse ${\mathcal {M_{V}}}\models A\to B$. Dunque, $\Gamma ,A\models B$ sse (${\mathcal {M_{V}}}\nvDash \Gamma$ oppure ${\mathcal {M_{V}}}\models A\to B$) sse $\Gamma \models A\to B$.

Completezza di insiemi di connettivi

I connettivi definiscono delle funzioni da ${\mathcal {B}}$ (nel caso del connettivo unario $\neg$), oppure ${\mathcal {B}}\times {\mathcal {B}}$ (nel caso dei connettivi binari) in ${\mathcal {B}}$. Ciascuna di queste funzioni, dette funzioni booleane, è definita attraverso la relativa tavola dei valori di verità, oppure, equivalentemente, attraverso le funzioni ${\mathcal {Op}}_{\neg }$ e ${\mathcal {Op}}_{\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 ${\mathcal {B}}^{n}$ in ${\mathcal {B}}$.

Funzione di verità

Definizione

Sia $A$ una formula della logica proposizionale contenente esattamente $n$ simboli proposizionali distinti $A_{1},...,A_{n}$; la funzione $f_{A}:{\mathcal {B}}^{n}\mapsto {\mathcal {B}}$ tale che $f_{A}(v_{1},...,v_{n})=I_{\mathcal {V}}(A)$, dove ${\mathcal {V}}$ è l'interpretazione per cui ${\mathcal {V}}(A_{i})=v_{i}$ per ogni $i=1,...,n$ è detta la funzione di verità associata ad $A$.

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 ${\mathcal {B}}^{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

Definizione

Dato un insieme di connettivi ${\mathcal {C}}$ e un connettivo $c\not \in {\mathcal {C}}$ per cui si abbia una funzione di verità $f_{c}={\mathcal {Op}}_{c}$, si dice che $c$ si deriva da (oppure si definisce in termini dei) connettivi di ${\mathcal {C}}$ se esiste una formula proposizionale $F$ costruita usando solo i connettivi di ${\mathcal {C}}$ tale che $f_{c}\equiv f_{F}$.

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 \bot )\to \bot )\to (B\to \bot ))\to \bot$
$\neg A$	$\equiv$	$A\to \bot$
$\bot$	$\equiv$	$A\land \neg A$
$A\leftrightarrow B$	$\equiv$	$(A\to B)\land (B\to A)$

Si noti che la costante proposizionale $\bot$ (così come la costante proposizionale $\top$) 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

Per approfondire, vedi Dimostrazione di completezza di insiemi di connettivi.

Definizione

Un insieme di connettivi logici ${\mathcal {C}}$ si dice funzionalmente completo sse, data una qualunque $f:{\mathcal {B}}^{n}\mapsto {\mathcal {B}}$ esiste una formula proposizionale $A$ costruita mediante i connettivi dell'insieme ${\mathcal {C}}$ tale che $f\equiv f_{A}$.

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 $\Gamma$ 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 \mathbb {N}$.

Lemma di enumerabilità

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

Dimostrazione

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

$\vDash A,$

$\Gamma _{0}\models A,$

$\Gamma _{1}\models A,$

$\qquad ...$

Per il corollario del teorema di compattezza, se $\Gamma \models A$ esiste un $\Gamma _{i}$ finito tale che $\Gamma _{i}\models A$, e dunque tale $\Gamma _{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 $\vdash$, per indicare che da una sentenza possiamo derivare sintatticamente un'altra sentenza.

Abbiamo così due concetti:

$A\models B$

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

$A\vdash 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 $\vdash _{s}\Phi$ allora $\vDash \Phi$.

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

La proprietà di completezza è:

se $\vDash \Phi$ allora $\vdash _{s}\Phi$.

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

I principali sistemi di dimostrazione

• Il sistema di Frege-Hilbert
• La deduzione naturale
• Il calcolo dei sequenti
• I tableaux semantici
• La risoluzione