Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert

L'approccio al problema della deduzione seguito nei sistemi assiomatici consiste nell'individuare un insieme di proposizioni da cui partire, come dei principi che ci permettano di ottenere altre proposizioni, e di limitare al minimo il numero di regole di inferenza. Le proposizioni da cui partire, che quindi vengono assunte come primitive, sono gli assiomi (logici).

Sono stati proposti vari sistemi assiomatici. Presentiamo qui di seguito quello introdotto da Hilbert, noto come sistema hilbertiano per la logica proposizionale. Il sistema di dimostrazione è stato proposto in modo formale da Hilbert, ma era già in uso dall'opera di Frege, per cui lo indichiamo con i due nomi. Si noti come questo sistema ricordi la geometria di Euclide: degli assiomi su cui non si discute e delle regole per derivare da questi nuove verità.

Definizione

Definizione

Siano $\phi$, $\psi$ e $\chi$ tre simboli proposizionali. Il calcolo proposizionale è definito dai seguenti schemi di assioma e dalle seguenti regole di inferenza.

1. Schemi di assioma

(a) $\phi \to (\psi \to \phi )$;

(b) $(\phi \to (\psi \to \chi ))\to ((\phi \to \psi )\to (\phi \to \chi ))$;

(c) $(\neg \psi \to \neg \phi )\to (\phi \to \psi )$.

2. Regole di inferenza

• Modus Ponens (MP)

$A,\quad A\to B \over B$

cioè, da $A$ e $A\to B$ è possibile derivare $B$.

• Sostituzione Uniforme (SU)

$F[p] \over F[X/p]$

dove $p$ è un simbolo proposizionale che può occorrere in $F$, $X$ è una proposizione e $p$ non occorre in $X$, $F[X/p]$ è detta un'istanza di $F[p]$.

Gli assiomi del sistema hilbertiano coinvolgono solo i connettivi $\to$ e $\neg$; vedremo nel seguito come estenderli agli altri connettivi. In effetti, è in virtù della sostituzione uniforme che possiamo parlare di schemi di assioma; in altri termini, l'insieme ${\text{AXIOM}}$ degli assiomi del calcolo proposizionale è l'insieme di tutte le formule che si ottengono sostituendo uniformemente proposizioni al posto dei simboli proposizionali negli schemi a, b e c. È dunque chiaro che l'insieme degli assiomi ${\text{AXIOM}}$ è un insieme infinito, poiché l'insieme delle istanze di a, b e c è infinito.

Altre possibili definizioni

Modus Tollens

Il modus tollens (MT) è un'altra possibile regola di inferenza:

$\neg B,\quad A\to B \over \neg A$ cioè, da $\neg B$ e $A\to B$ è possibile derivare $\neg A$.

L'assioma di Meredith

Un logico Irlandese, Carew Meredith, nel 1953 ha proposto un singolo schema di assioma, che può sostituire i tre schemi che abbiamo visto sopra.

Lo schema è:

$(((A\to B)\to (\neg C\to \neg D))\to C)\to (E\to ((E\to A)\to (D\to A)))$.

I logici credono, ma non è ancora stato provato, che questa sia la singola formula più corta possibile da cui può essere derivato l'intero calcolo delle proposizioni basato su implicazione e negazione e con le sole regole deduttive MP e SU.

Relazione di derivazione

Seguendo le definizioni di dimostrazione e di teorema, diciamo che una sequenza $A_{1},...,A_{n}$ è una dimostrazione di $A$ sse $A_{n}=A$ e, per ogni $i$, $1\leq i\leq n$, $A_{i}$ è un'istanza di uno schema di assioma (cioè, è ottenuto da a, b e c per mezzo di SU), oppure $A_{i}$ è ottenuto da $A_{j}$ e $A_{k}$, $j,k<i$, per MP, dove $A_{k}=A_{j}\to A_{i}$. In tal caso, $A$ è un teorema del calcolo proposizionale e lo indichiamo:

$\vdash _{H}A$

che si legge "$A$ è dimostrabile", dove il pedice $H$ sta a indicare che la dimostrazione è stata fatta con l'apparato deduttivo hilbertiano. Diciamo che una proposizione $A$ ha una prova da un insieme di proposizioni $\Gamma$ se esiste una derivazione $A_{1},...,A_{n}=A$ tale che, per ogni $i$, $1\leq i\leq n$, $A_{i}$ è un'istanza di uno schema di assioma (cioè, è ottenuto da a, b e c per mezzo di SU), oppure $A_{i}$ è ottenuto da $A_{j}$ e $A_{k}$, $j,k<i$, per MP, dove $A_{k}=A_{j}\to A_{i}$, o $A_{i}$ è in $\Gamma$. Se $A$ ha una dimostrazione da $\Gamma$, scriviamo:

$\Gamma \vdash _{H}A$

che si legge "da $\Gamma$ si deriva $A$". Gli elementi di $\Gamma$ sono chiamati premesse, o ipotesi, o anche dipendenze di $A$. Dalla definizione di dimostrazione, è evidente che

$\vdash _{H}A$ implica $\Gamma \vdash _{H}A$ per qualunque $\Gamma$

quindi, in particolare,

$\Gamma \vdash _{H}A$ per ogni $A\in {\text{AXIOM}}$.

Nel seguito, non essendoci possibilità di confusione, ometteremo il pedice $H$; inoltre, se $A$ ha una dimostrazione da $\Gamma \cup \{B\}$, scriviamo $\Gamma ,B\vdash A$. Scriviamo $\Delta \vdash \Gamma$ per indicare che $\Delta \vdash A$ per ogni formula $A\in \Gamma$.

Proprietà

Illustriamo ora le proprietà della relazione di derivazione $\vdash$. Diciamo che $\vdash$ è una relazione, in quanto $\vdash \subseteq {\mathcal {\wp L\times L}}$.

Le seguenti sono proprietà della relazione di derivazione $\vdash$ nel calcolo proposizionale:

1. Inclusione: Se $A\in \Gamma$ allora $\Gamma \vdash A$;
2. Monotonia: Se $\Gamma \subseteq \Delta$ e $\Gamma \vdash A$ allora $\Delta \vdash A$;
3. Compattezza: $\Gamma \vdash A$ sse esiste un $\Gamma _{0}$ finito, tale che $\Gamma _{0}\subseteq \Gamma$ e $\Gamma _{0}\vdash A$;
4. Taglio: Se $\Delta \vdash A$ e per ogni $B\in \Delta$ si ha che $\Gamma \vdash B$, allora $\Gamma \vdash A$.

Dimostrazione

1. Inclusione. Sia $A\in \Gamma$, dalla definizione di dimostrazione di $A$ da $\Gamma$ segue che $\Gamma \vdash A$.

2. Monotonia. Sia $\Gamma \vdash A$, dunque esiste una dimostrazione $A_{1},...,A_{n}=A$, da $\Gamma$ per $A$. Procediamo per induzione completa.

(Passo base) $A_{1}\in \Gamma$ oppure $A_{1}$ è un assioma. Se $A_{1}\in \Gamma \subseteq \Delta$, allora $A_{1}\in \Delta$, dunque, per inclusione, $\Delta \vdash A_{1}$; se $A_{1}$ è un'istanza di assioma, allora $\Delta \vdash A_{1}$.

(Passo induttivo) Supponiamo vero per ogni $i<n$ che $\Delta \vdash A_{i}$. Se $A_{n}\in \Gamma$ o $A_{n}$ è un'istanza di assioma, allora, come sopra, $\Delta \vdash A_{n}$. Se $A_{n}$ è stato derivato mediante MP, lo si è ottenuto da $A_{j}$, $A_{k}=A_{j}\to A_{n}$, $j,k<n$, ma per ipotesi induttiva $\Delta \vdash A_{j}$ e $\Delta \vdash A_{j}\to A_{n}$, pertanto, per MP, $\Delta \vdash A_{n}$.

3. Compattezza. Se $\Gamma \vdash A$, allora esiste una dimostrazione $A_{1},...,A_{n}=A$ da $\Gamma$. Se nessun $A_{i}\in \Gamma$, allora $\vdash A$, dunque la tesi è vera. Altrimenti, consideriamo l'insieme $\Gamma _{0}$ degli $A_{i}$ che occorrono nella dimostrazione di $A$ tali che $A_{i}\in \Gamma$. Tale insieme è finito. Siccome per ogni altro $A_{j}$ che occorre nella dimostrazione di $A$ abbiamo che o è un'istanza di uno schema di assioma, o è ottenuto da due precedenti proposizioni per MP, ne segue che $\Gamma _{0}\vdash A$. Viceversa, supponiamo che $\Gamma _{0}\vdash A$; per monotonia, poiché $\Gamma _{0}\subseteq \Gamma$, abbiamo $\Gamma \vdash A$. (Si può notare che una direzione della compattezza è per l'appunto la monotonia).

4. Taglio. Supponiamo $\Delta \vdash A$ e, per ogni $B\in \Delta$, $\Gamma \vdash B$. Consideriamo una derivazione $B_{1},...,B_{n}=A$ di $A$ da $\Delta$. Se $\Delta$ è vuoto, la tesi è dimostrata. Altrimenti, per ogni $B_{i}\in \Delta$, avremo per ipotesi una dimostrazione $B_{k_{1}},...,B_{k_{i}}=B_{i}$ da $\Gamma$. Possiamo quindi sostituire in $B_{1},...,B_{n}=A$ ciascun $B_{i}\in \Delta$ con la relativa dimostrazione a partire da $\Gamma$, ottenendo la sequenza $B_{1},...,B_{k_{1}},...,B_{k_{i}}=B_{i},...,B_{l_{1}},...,B_{l_{j}}=B_{j},...,B_{n}=A$. Questa sequenza è una dimostrazione di $A$ da $\Gamma$, quindi $\Gamma \vdash A$.

Introduzione di ulteriori connettivi

Come accennato in precedenza, altri connettivi possono essere introdotti mediante definizioni, ad esempio:

1. $A\land B=_{Def}\neg (A\to \neg B)$;
2. $A\lor B=_{Def}\neg A\to B$;
3. $A\leftrightarrow B=_{Def}(A\to B)\land (B\to A)$.

Osserviamo che, in questo contesto, abbiamo dato delle definizioni per i connettivi perché non possiamo utilizzare la nozione di completezza di insiemi di connettivi, che si basa sulla nozione di valutazione booleana. Qui, infatti, stiamo solo considerando un "calcolo", che è una nozione puramente sintattica, dunque non siamo autorizzati a utilizzare nozioni semantiche, quali l'equivalenza logica. Non possiamo usare nozioni semantiche fintantoché non dimostreremo un teorema che ci dice che "possiamo utilizzare le tautologie come teoremi", ovvero il teorema di completezza.

Teorema di deduzione

Sia $\Gamma$ un insieme di formule proposizionali e siano $A$ e $B$ due formule proposizionali, allora

$\Gamma ,B\vdash A$ sse $\Gamma \vdash B\to A$.

Dimostrazione

($\Rightarrow$) Sia $A_{1},...,A_{n}=A$ una dimostrazione di $A$ da $\Gamma \cup \{B\}$. Procediamo per induzione completa.

(Passo base) $A_{1}\in \Gamma$, oppure $A_{1}$ è un assioma, oppure è $B$ stesso. Per lo schema a abbiamo $A_{1}\to (B\to A_{1})$, dunque, se $A_{1}\in \Gamma$ o $A_{1}$ è un assioma, abbiamo per MP che $\Gamma \vdash B\to A_{1}$. Se $A_{1}=B$, siccome $B\to B$ è un teorema, abbiamo $\Gamma \vdash B\to B$.

(Passo induttivo) Supponiamo che $\Gamma \vdash B\to A_{i}$, per ogni $i<n$. Consideriamo $A_{n}$. Come sopra, se $A_{n}\in \Gamma$ o $A_{n}$ è un assioma o $A_{n}=B$ abbiamo che $\Gamma \vdash B\to A_{n}$. Supponiamo allora che $A_{n}$ sia stato derivato per MP. Dunque, lo si è ottenuto da due formule $A_{j}$, $A_{k}=A_{j}\to A_{n}$, $j,k<n$. Per ipotesi induttiva, $\Gamma \vdash B\to A_{j}$ e $\Gamma \vdash B\to A_{k}$. $A_{k}$ è della forma $A_{j}\to A_{n}$, dunque abbiamo $\Gamma \vdash B\to (A_{j}\to A_{n})$. Per lo schema di assioma b, abbiamo che $(B\to (A_{j}\to A_{n}))\to ((B\to A_{j})\to (B\to A_{n}))$. Da questa formula, da $B\to (A_{j}\to A_{n})$ e da $B\to A_{j}$, applicando due volte MP, si ha $\Gamma \vdash B\to A_{n}$.

($\Leftarrow$) Supponiamo che $\Gamma \vdash B\to A$. Per monotonia abbiamo che $\Gamma ,B\vdash B\to A$. Per inclusione, invece, si ha che $\Gamma ,B\vdash B$. Dunque, per MP si ottiene che $\Gamma ,B\vdash A$.

Osservazioni

Il teorema di deduzione ci dice che una formula può passare da sinistra a destra della relazione $\vdash$ introducendo il connettivo $\to$, oppure da destra a sinistra eliminandolo. Questo risultato è importante per due ragioni. In primo luogo, perché ci fornisce la possibilità di esprimere una relazione metalinguistica (quale $\vdash$) mediante una formula del linguaggio.

In secondo luogo, esso ci fornisce la possibilità di trattare generiche derivazioni da insiemi di formule come teoremi. Infatti, in virtù della proprietà di compattezza di $\vdash$, abbiamo che, se $\Gamma \vdash A$, allora esiste un insieme finito $\Gamma _{0}\subseteq \Gamma$ tale che $\Gamma _{0}\vdash A$. Siccome $\Gamma _{0}$ è finito, sarà del tipo $\{A_{1},...,A_{n}\}$, o equivalentemente $\{A_{1}\land ...\land A_{n}\}$, quindi $\Gamma \vdash A$ implica $\Gamma _{0}\vdash A$, che equivale a $A_{1}\land ...\land A_{n}\vdash A$ e $A_{1},...,A_{n}\vdash A$. Per il teorema di deduzione, otteniamo $\vdash (A_{1}\land ...\land A_{n})\to A$ e $\vdash A_{1}\to (...\to (A_{n}\to A)...)$.

Consistenza

Introduciamo ora la nozione di consistenza.

Insieme di formule consistente

Definizione

Un insieme di formule proposizionali $\Gamma$ è consistente sse è verificata una delle seguenti proprietà:

1. non esiste una proposizione $A$ tale che $\Gamma \vdash A$ e $\Gamma \vdash \neg A$;
2. esiste una proposizione $A$ tale che $\Gamma \nvdash A$.

Si può dimostrare che le due formulazioni sono equivalenti.

($\Rightarrow$) Se non esiste una proposizione $A$ tale che $\Gamma \vdash A$ e $\Gamma \vdash \neg A$, allora si ha che $\Gamma \nvdash A$ oppure $\Gamma \nvdash \neg A$ per ogni proposizione $A$, dunque esiste una proposizione $B$ tale che $\Gamma \nvdash B$.

($\Leftarrow$) Scriviamo la tesi in forma contrappositiva: se esiste una proposizione $A$ tale che $\Gamma \vdash A$ e $\Gamma \vdash \neg A$, allora non esiste una formula $B$ tale che $\Gamma \nvdash B$, che equivale a dire $\Gamma \vdash B$ per ogni formula $B$.

Se si dimostra che $\neg A,A\vdash B$ per ogni formula $B$, allora, per taglio sulle premesse, si ha che $\Gamma \vdash B$.

Per il teorema di deduzione, abbiamo che $\vdash \neg A\to (A\to B)$. Dunque, $\neg A,A\vdash B$ sse $\vdash \neg A\to (A\to B)$.

Essendo $\neg A\to (A\to B)$ un teorema, effettivamente vale $\neg A,A\vdash B$, e, per taglio sulle premesse, si ha che $\Gamma \vdash B$ per ogni formula $B$.

Dunque, per contrapposizione, se esiste una formula $B$ tale che $\Gamma \nvdash B$, allora non esiste una proposizione $A$ tale che $\Gamma \vdash A$ e $\Gamma \vdash \neg A$.

Insieme di formule completo

Definizione

Un insieme di formule $\Gamma$ si dice consistente e massimale o completo se, per ogni formula $A\in {\mathcal {L}}$, si verifica una e una sola delle seguenti relazioni:

$\Gamma \vdash A$ oppure $\Gamma \vdash \neg A$.

Notare che la nozione di insieme consistente e massimale è analoga a quella di insieme massimale soddisfacibile.

Correttezza e completezza

Precedentemente, sono state introdotte le nozioni di "dimostrazione", "teorema", "assioma", "derivazione", ecc. e abbiamo mostrato delle utili proprietà della relazione $\vdash$.

Illustriamo ora la relazione che lega i teoremi e le tautologie. La domanda che ci poniamo è: tutto ciò che deriviamo mediante $\vdash$ senza premesse è vero in tutti i modelli della logica?

In secondo luogo, vogliamo sapere in che relazione stanno le formule proposizionali derivabili da un insieme di proposizioni $\Gamma$ con le formule vere nei modelli di $\Gamma$. Supponiamo che $\Gamma$ sia un insieme di proposizioni che descrivono una determinata realtà; quando deriviamo un enunciato $A$ da $\Gamma$, è importante sapere se $A$ è vero nelle realtà che sono modelli di $\Gamma$. Ovvero, ci interessa sapere se c'è una corrispondenza effettiva tra ciò che consegue dalle premesse e ciò che è vero nelle strutture che interpretano tali premesse.

Per verificare questa corrispondenza, dobbiamo mostrare che:

(i) l'insieme delle tautologie coincide con l'insieme dei teoremi

$\vdash A$ sse $\vDash A$;

(ii) ciò che deriva da un insieme $\Gamma$ è vero in tutti i modelli di $\Gamma$

$\Gamma \vdash A$ sse $\Gamma \vDash A$.

La proprietà al punto i è detta correttezza e completezza debole, mentre quella al punto ii è detta correttezza e completezza forte. In effetti, per le logiche in cui, come nel nostro caso, vale un teorema di compattezza e di deduzione, i due enunciati sono equivalenti: $\Gamma \vdash B$ può essere scritto come $\vdash (A_{1}\land ...\land A_{n})\to B$, dove $(A_{1}\land ...\land A_{n})$ è la congiunzione delle formule di $\Gamma$.

Dire che l'insieme dei teoremi è parte dell'insieme delle tautologie assicura che l'apparato deduttivo è corretto, non può infatti dimostrare formule non valide o contraddittorie. Dire che l'insieme delle tautologie è parte dell'insieme dei teoremi assicura che l'apparato deduttivo è completo, cioè che tutte le formule valide sono dimostrabili.

L'insieme dei teoremi del sistema deduttivo hilbertiano può essere definito induttivamente: esso è l'insieme generato dagli schemi di assioma e chiuso rispetto alle regole di MP e SU. Pertanto, la correttezza si può dimostrare induttivamente.

Più difficile da dimostrare è invece la completezza, perché l'insieme delle tautologie non è definito induttivamente.

Teorema di correttezza

$\Gamma \vdash A$ implica $\Gamma \vDash A$.

Dimostrazione

È sufficiente dimostrare che:

1. gli schemi a, b e c sono tautologie;
2. MP e SU sono chiusi rispetto alla conseguenza logica. Ovvero, se $A$ e $A\to B$ sono soddisfatte da $\Gamma$, anche $B$ è soddisfatta da $\Gamma$, e se $F[p]$ è una tautologia, anche $F[X/p]$ lo è.
3. Ogni formula di una dimostrazione per $A$ da $\Gamma$ è soddisfatta da $\Gamma$.

La verifica che a, b e c sono tautologie è banale.

Verifichiamo che MP è chiuso rispetto alla conseguenza logica. Supponiamo per assurdo che $\Gamma \models A$ e $\Gamma \models A\to B$, ma $\Gamma \nvDash B$. Se $\Gamma \nvDash B$, allora esiste un modello ${\mathcal {M_{V}}}$ tale che ${\mathcal {M_{V}}}\vDash \Gamma$ e ${\mathcal {M_{V}}}\nvDash B$; ma $A$ è soddisfatta da $\Gamma$, perciò è verificata in ${\mathcal {M_{V}}}$. Pertanto, ${\mathcal {M_{V}}}\models A$ e ${\mathcal {M_{V}}}\nvDash B$ e, per definizione di implicazione, ${\mathcal {M_{V}}}\nvDash A\to B$. Dunque, essendo che ${\mathcal {M_{V}}}\vDash \Gamma$, $\Gamma \nvDash A\to B$; contraddizione.

Per quanto riguarda la SU, sia $F[p]$ una tautologia. Allora, $\vDash F[p]$ per qualunque assegnazione booleana alle lettere proposizionali di $F[p]$, in particolare a $p$; dunque, per qualunque proposizione $X$ possiamo porre $I_{\mathcal {V}}(p)=I_{\mathcal {V}}(X)$. Per il teorema del rimpiazzamento, $I_{\mathcal {V}}(F[p/p])=I_{\mathcal {V}}(F[X/p])$, da cui segue $\vDash F[X/p]$.

Dimostriamo ora il punto 3. Sia $A_{1},...,A_{n}=A$ una dimostrazione da $\Gamma$ per $A$. Procediamo per induzione completa.

(Passo base) $\Gamma \vDash A_{1}$ vale sse, per ogni modello ${\mathcal {M_{V}}}$, se ${\mathcal {M_{V}}}\vDash \Gamma$ allora ${\mathcal {M_{V}}}\vDash A_{1}$. $A_{1}\in \Gamma$ oppure $A_{1}$ è un assioma. Se $A_{1}\in \Gamma$, allora abbiamo $\Gamma \vDash A_{1}$ per definizione di modello; se $A_{1}$ è un'istanza di assioma, allora, essendo SU chiuso rispetto alla conseguenza logica, $\vDash A_{1}$, dunque $\Gamma \models A_{1}$.

(Passo induttivo) Supponiamo vero per ogni $i<n$ che $\Gamma \models A_{i}$. Se $A_{n}\in \Gamma$ o $A_{n}$ è un'istanza di assioma, allora, come sopra, $\Gamma \models A_{n}$. Se $A_{n}$ è stato derivato mediante MP, lo si è ottenuto da $A_{j}$, $A_{k}=A_{j}\to A_{n}$, $j,k<n$, ma per ipotesi induttiva $\Gamma \models A_{j}$ e $\Gamma \models A_{k}$, pertanto, essendo MP chiuso rispetto alla conseguenza logica, $\Gamma \models A_{n}$.

Teorema di completezza

$\Gamma \vDash A$ implica $\Gamma \vdash A$.

Per dimostrare il teorema di completezza, ci serviamo dei seguenti lemmi.

Lemma 1

Sia $\Gamma$ un insieme di formule e sia $A$ una formula. $\Gamma \vdash A$ sse $\Gamma \cup \{\neg A\}$ è inconsistente.

Dimostrazione

($\Rightarrow$) Supponiamo che $\Gamma \vdash A$. Allora, per monotonia, $\Gamma ,\neg A\vdash A$. Dal momento che, per inclusione, $\Gamma ,\neg A\vdash \neg A$, $\Gamma \cup \{\neg A\}$ è inconsistente.

($\Leftarrow$) Supponiamo che $\Gamma \cup \{\neg A\}$ sia inconsistente. Allora da esso è possibile derivare qualsiasi formula, dunque abbiamo che $\Gamma ,\neg A\vdash A$. Per il teorema di deduzione, si ha che $\Gamma \vdash \neg A\to A$. Essendo $(\neg A\to A)\to A$ un teorema, per MP otteniamo $\Gamma \vdash A$.

Lemma 2

Se $\Gamma$ è un insieme di formule consistente, allora, per ogni formula $A$, $\Gamma \cup \{A\}$ oppure $\Gamma \cup \{\neg A\}$ è consistente.

Dimostrazione

Supponiamo, per assurdo, che $\Gamma$ sia consistente, ma sia $\Gamma \cup \{A\}$ che $\Gamma \cup \{\neg A\}$ siano inconsistenti. Siccome $\Gamma \cup \{A\}$ è inconsistente, per il lemma 1 abbiamo che $\Gamma \vdash \neg A$. Ma, essendo pure $\Gamma \cup \{\neg A\}$ inconsistente, abbiamo anche $\Gamma \vdash A$. Dunque, $\Gamma$ è inconsistente; contraddizione.

Lemma 3

Sia $\Gamma$ un insieme di formule. Se $\Gamma$ è insoddisfacibile, allora $\Gamma$ è inconsistente.

Dimostrazione

Dimostriamo la tesi in forma contrappositiva: se $\Gamma$ è consistente, allora $\Gamma$ è soddisfacibile.

Supponiamo che $\Gamma$ sia consistente.

Sia $A_{0},A_{1},A_{2}...$ l'enumerazione di tutte le formule del linguaggio ${\mathcal {L}}$. Definiamo, per induzione, una sequenza di insiemi di formule:

$\Delta _{0}=\Gamma ;$

$\Delta _{i+1}={\begin{cases}\Delta _{i}\cup \{A_{i}\},&{\text{se }}\Delta _{i}\cup \{A_{i}\}{\text{ è consistente;}}\\\Delta _{i}\cup \{\neg A_{i}\},&{\text{altrimenti.}}\end{cases}}$

Per ogni $i\in \mathbb {N}$, l'esistenza di $\Delta _{i}$ è giustificata dal lemma 2 e, per costruzione, ogni $\Delta _{i}$ è consistente.

Sia $\Delta =\bigcup _{i}\Delta _{i}$. Osserviamo che

1. $\Gamma \subseteq \Delta$, per costruzione.
2. $\Delta$ è massimale, cioè, per ogni formula $F$, $F$ o la sua negazione appartengono a $\Delta$. Infatti, siccome l'enumerazione delle formule è completa, per costruzione dei $\Delta _{i}$, presa una qualunque $F$, esisterà un $i$ per cui $F=A_{i}$, quindi $F\in \Delta _{i}\subseteq \Delta$ oppure $\neg F\in \Delta _{i}\subseteq \Delta$.
3. Ciascun $\Delta _{i}$ è consistente (per induzione: $\Delta _{0}=\Gamma$ è consistente; il passo induttivo è giustificato dal lemma 2).
4. $\Delta$ è consistente. Supponiamo per assurdo che non lo sia. Allora esiste una formula $F$ tale che $\Delta \vdash F$ e $\Delta \vdash \neg F$. Quindi, per compattezza, esistono due insiemi finiti $\Delta _{i},\Delta _{j}\subseteq \Delta$ tali che $\Delta _{i}\vdash F$ e $\Delta _{j}\vdash \neg F$. Per costruzione, abbiamo che $\Delta _{i}\subseteq \Delta _{j}$ oppure $\Delta _{j}\subseteq \Delta _{i}$. Se $\Delta _{i}\subseteq \Delta _{j}$, per monotonia si ha che $\Delta _{j}\vdash F$, dunque $\Delta _{j}$ è inconsistente, contraddizione con il punto 3. Viceversa, se $\Delta _{j}\subseteq \Delta _{i}$, per monotonia si ha che $\Delta _{i}\vdash \neg F$, dunque $\Delta _{i}$ è inconsistente, contraddizione con il punto 3.
5. Per ogni formula $F$, $\neg F\in \Delta$ sse $F\not \in \Delta$. Supponiamo che $F\not \in \Delta$. Allora, essendo $\Delta$ massimale, abbiamo che $\neg F\in \Delta$. Supponiamo per assurdo che $\neg F\in \Delta$, ma $F\in \Delta$. Allora, per inclusione, si ha che $\Delta \vdash \neg F$ e $\Delta \vdash F$, dunque, $\Delta$ è inconsistente. Contraddizione con il punto 4.
6. Per ogni formula $F$, se $\Delta \vdash F$ allora $F\in \Delta$. Supponiamo per assurdo che $\Delta \vdash F$, ma $F\not \in \Delta$. Allora, per il punto 5, abbiamo che $\neg F\in \Delta$, quindi, per inclusione, $\Delta \vdash \neg F$, dunque, $\Delta$ è inconsistente. Contraddizione con il punto 4.
7. Per ogni formula $A$ e $B$, $A\to B\in \Delta$ sse $A\not \in \Delta$ o $B\in \Delta$. Supponiamo per assurdo che $A\to B\in \Delta$, $A\in \Delta$ e $B\not \in \Delta$. Per inclusione, abbiamo che $\Delta \vdash A\to B$ e $\Delta \vdash A$, pertanto, per MP, $\Delta \vdash B$ e, per il punto 6, $B\in \Delta$; contraddizione. Se $A\not \in \Delta$, allora, per il punto 5, $\neg A\in \Delta$. Per inclusione, abbiamo che $\Delta \vdash \neg A$. Essendo $\neg A\to (A\to B)$ un teorema, per MP otteniamo $\Delta \vdash A\to B$, dunque $A\to B\in \Delta$. Se $B\in \Delta$, allora, per inclusione, abbiamo $\Delta \vdash B$. Per monotonia, si ha che $\Delta ,A\vdash B$, quindi, per il teorema di deduzione, otteniamo $\Delta \vdash A\to B$, dunque $A\to B\in \Delta$.

Dobbiamo ora mostrare che $\Delta$ è soddisfacibile. Per far questo, costruiamo un modello per esso. Definiamo il modello ${\mathcal {M_{V}}}$ come:

${\mathcal {M_{V}}}=\{p|p\in {\mathcal {P}},p\in \Delta \}$

dove ${\mathcal {P}}$ è l'insieme dei simboli proposizionali del linguaggio. Dimostriamo ora, per induzione strutturale sulle formule, che per ogni formula $F$:

${\mathcal {M_{V}}}\models F$ sse $F\in \Delta$.

(Passo base) Per costruzione di ${\mathcal {M_{V}}}$.

(Passo induttivo) Sia $F=\neg A$. Abbiamo che ${\mathcal {M_{V}}}\models \neg A$ sse ${\mathcal {M_{V}}}\nvDash A$ (per definizione) sse $A\not \in \Delta$ (per ipotesi induttiva) sse $\neg A\in \Delta$ (per il punto 5).

Sia $F=A\to B$. Abbiamo che ${\mathcal {M_{V}}}\models A\to B$ sse ${\mathcal {M_{V}}}\nvDash A$o ${\mathcal {M_{V}}}\models B$ (per definizione) sse $A\not \in \Delta$ o $B\in \Delta$ (per ipotesi induttiva) sse $A\to B\in \Delta$ (per il punto 7).

Abbiamo quindi mostrato che ${\mathcal {M_{V}}}$ è un modello per $\Delta$; siccome $\Gamma \subseteq \Delta$, abbiamo che ${\mathcal {M_{V}}}\models \Gamma$, ovvero $\Gamma$ è soddisfacibile.

Dimostrazione

Supponiamo che $\Gamma \vDash A$. Allora, per il teorema di soddisfacibilità, $\Gamma \cup \{\neg A\}$ è insoddisfacibile e, per il lemma 3, è anche inconsistente. Dunque, per il lemma 1, $\Gamma \vdash A$.

Regole derivate

Le seguenti sono regole derivate dal MP e gli schemi di assioma, per permettere di utilizzare agevolmente il sistema di Hilbert.

Regola di deduzione

$\Gamma ,A\vdash B \over \Gamma \vdash A\to B$

Equivalente al teorema di deduzione.

Regola di contrapposizione

$\neg B\to \neg A \over A\to B$

Si deriva dallo schema c con il teorema di deduzione.

Regola di transitività

$A\to B,\quad B\to C \over A\to C$

Corrisponde al sillogismo ipotetico.

Regola di scambio delle premesse

$A\to (B\to C) \over B\to (A\to C)$

Dimostrazione

1. $\Gamma \vdash A\to (B\to C)$: ipotesi;
2. $\Gamma ,A\vdash B\to C$: teorema di deduzione su 1;
3. $\Gamma ,A,B\vdash C$: teorema di deduzione su 2;
4. $\Gamma ,B\vdash A\to C$: teorema di deduzione su 3;
5. $\Gamma \vdash B\to (A\to C)$: teorema di deduzione su 4.

Dunque, $\Gamma \vdash A\to (B\to C)$ sse $\Gamma \vdash B\to (A\to C)$.

Regola dello Pseudo-Scoto

$A,\quad \neg A \over B$

Dimostrazione

Da $\vdash \neg A\to (A\to B)$ (teorema dello Pseudo-Scoto), per il teorema di deduzione, si ha che $\neg A,A\vdash B$.

Consequentia mirabilis

$\vdash (\neg A\to A)\to A$

Dimostrazione

1. $\neg A\to A$: ipotesi;
2. $\vdash \neg A\to (A\to \neg (\neg A\to A))$: SU sul teorema dello Pseudo-Scoto;
3. $\vdash (\neg A\to (A\to \neg (\neg A\to A)))\to ((\neg A\to A)\to (\neg A\to \neg (\neg A\to A)))$: SU in b;
4. $\vdash (\neg A\to A)\to (\neg A\to \neg (\neg A\to A))$: MP tra 2 e 3;
5. $\neg A\to \neg (\neg A\to A)$: MP tra 1 e 4;
6. $(\neg A\to A)\to A$: contrapposizione di 5;
7. $A$: MP tra 1 e 6.

Quindi, $\neg A\to A\vdash A$. Dunque, per il teorema di deduzione, $\vdash (\neg A\to A)\to A$.

Eliminazione della doppia negazione

$\neg \neg A \over A$

Dimostrazione

1. $\neg \neg A$: ipotesi;
2. $\vdash \neg \neg A\to (\neg A\to A)$: SU sul teorema dello Pseudo-Scoto;
3. $\neg A\to A$: MP tra 1 e 2;
4. $\vdash (\neg A\to A)\to A$: Consequentia mirabilis;
5. $A$: MP tra 3 e 4.

Dunque, $\neg \neg A\vdash A$, quindi, per il teorema di deduzione, $\vdash \neg \neg A\to A$.

Introduzione della doppia negazione

$A \over \neg \neg A$

Dimostrazione

1. $\vdash \neg \neg A\to A$: eliminazione della doppia negazione;
2. $\vdash \neg \neg \neg A\to \neg A$: SU in 1 con $\neg A$ al posto di $A$;
3. $\vdash A\to \neg \neg A$: contrapposizione di 2;
4. $A\vdash \neg \neg A$: teorema di deduzione su 3.

Modus Tollens

$\neg B,\quad A\to B \over \neg A$

Dimostrazione

1. $A\to B$: ipotesi;
2. $\neg B$: ipotesi;
3. $\vdash \neg \neg A\to A$: eliminazione della doppia negazione;
4. $\neg \neg A\to B$: sillogismo ipotetico tra 3 e 1;
5. $\vdash B\to \neg \neg B$: introduzione della doppia negazione;
6. $\neg \neg A\to \neg \neg B$: sillogismo ipotetico tra 4 e 5;
7. $\neg B\to \neg A$: contrapposizione di 6;
8. $\neg A$: MP tra 2 e 7.

Dunque, $\neg B,A\to B\vdash \neg A$.

Applicando il teorema di deduzione, abbiamo la contrapposizione all'inverso: $A\to B\vdash \neg B\to \neg A$.

Esempi di dimostrazioni

Riflessività dell'implicazione

Dimostriamo che $\vdash A\to A$.

1. $\vdash (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))$: SU sullo schema b con $A$ al posto di $\phi$ e $\chi$, $B\to A$ al posto di $\psi$;
2. $\vdash A\to ((B\to A)\to A)$: SU in a con $A$ al posto di $\phi$ e $B\to A$ al posto di $\psi$;
3. $\vdash (A\to (B\to A))\to (A\to A)$: MP tra 1 e 2;
4. $\vdash (A\to (B\to A))$: SU in a con $A$ al posto di $\phi$ e $B$ al posto di $\psi$;
5. $\vdash A\to A$: MP tra 3 e 4.

Sillogismo ipotetico

Dimostriamo che $A\to B,B\to C\vdash A\to C$.

1. $A$: ipotesi;
2. $A\to B$: ipotesi;
3. $B$: MP tra 1 e 2;
4. $B\to C$: ipotesi;
5. $C$: MP tra 3 e 4.

Così abbiamo dimostrato che $A,A\to B,B\to C\vdash C$.

Applicando il teorema di deduzione (se $A\vdash C$ allora $\vdash A\to C$), otteniamo il risultato voluto, eliminando $A$ dalle ipotesi che abbiamo utilizzato.

Teorema dello Pseudo-Scoto

Dimostriamo che $\vdash \neg A\to (A\to B)$.

1. $\neg A$: ipotesi;
2. $\vdash \neg A\to (\neg B\to \neg A)$: SU in a;
3. $\neg B\to \neg A$: MP tra 1 e 2;
4. $A\to B$: contrapposizione di 3.

Abbiamo dimostrato che $\neg A\vdash A\to B$. Dunque, per il teorema di deduzione, $\vdash \neg A\to (A\to B)$.