Wikibooks

Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert: differenze tra le versioni

Naviga nella cronologia in modo interattivo
← Differenza precedenteDifferenza successiva →
Contenuto cancellato Contenuto aggiunto
VisualeWikitesto
Riga 6:
{{Definizione|
Siano <math>
\phi
A
</math>, <math>
\psi
B
</math> e <math>
\chi
C
</math> tre simboli proposizionali. Il calcolo proposizionale è definito dai seguenti schemi di assioma e dalle seguenti regole di inferenza.
 
Riga 16:
 
:''(a)'' <math>
A\phi \to (B\psi \to A\phi)
</math>;
:''(b)'' <math>
(A\phi \to (B\psi \to C\chi)) \to ((A\phi \to B\psi) \to (A\phi \to C\chi))
</math>;
:''(c)'' <math>
(\neg B\psi \to \neg A\phi) \to ((\neg Bphi \to A) \to Bpsi)
</math>.
 
Riga 55:
==== 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 utilizzatovisto finorasopra.
 
Lo schema è:
 
<math>
(((A \to B) \to (\neg C \to \neg D)) \to C) \to (E
\to ((E \to A) \to (D \to A)))
</math>.
 
Riga 148:
(<math>\Leftarrow</math>) Scriviamo la tesi in forma contrappositiva: se esiste una proposizione <math>A</math> tale che <math>\Gamma \vdash A</math> e <math>\Gamma \vdash \neg A</math>, allora non esiste una formula <math> B</math> tale che <math>\Gamma \nvdash B</math>, che equivale a dire <math>\Gamma \vdash B</math> per ogni formula <math> B</math>.
 
Se si dimostra che <math>A, \neg A, A \vdash B </math> per ogni formula <math> B</math>, allora, per taglio sulle premesse, si ha che <math>\Gamma \vdash B</math>.
 
Per il teorema di deduzione, abbiamo che <math> \vdash \neg A \to (\neg A \to B) </math>. Dunque, <math>A, \neg A, A \vdash B </math> sse <math> \vdash \neg A \to (\neg A \to B) </math>.
 
Essendo che <math> \vDashneg A \to (\neg A \to B) </math>, allora, per ilun [[Logica/Calcolo delle proposizioni/Sistema di Hilbert#TeoremaEsempi di completezzadimostrazioni|teorema di completezza]], èeffettivamente vero chevale <math>\vdash A \to (\neg A \to B)</math>. Quindi, effettivamente vale <math>A, \neg A \vdash B </math>, e, per taglio sulle premesse, si ha che <math>\Gamma \vdash B</math> per ogni formula <math> B</math>.
 
Dunque, per contrapposizione, se esiste una formula <math> B</math> tale che <math>\Gamma \nvdash B</math>, allora non esiste una proposizione <math>A</math> tale che <math>\Gamma \vdash A</math> e <math>\Gamma \vdash \neg A</math>.
Riga 192:
 
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: <math>\Gamma \vdash B</math> può essere scritto come <math>\vdash (A_1 \and ... \and A_n) \to B</math>, dove <math>(A_1 \and ... \and A_n)</math> è la congiunzione delle formule di <math>\Gamma</math>.
 
Pertanto, ci limitiamo a dimostrare
 
:<math>\vdash A \to B</math> sse <math>\vDash A \to B</math>.
 
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.
Line 205 ⟶ 201:
=== Teorema di correttezza ===
 
:<math>\Gamma \vdash A \to B</math> implica <math>\Gamma \vDash A \to B</math>.
 
==== Dimostrazione ====
Line 211 ⟶ 207:
 
# gli schemi ''a'', ''b'' e ''c'' sono tautologie;
# MP e SU sono chiusi rispetto alla conseguenza logica. Ovvero, se <math>A</math> e <math>A \to B</math> sono tautologiesoddisfatte da <math>\Gamma</math>, anche <math>B</math> è unasoddisfatta tautologiada <math>\Gamma</math>, e se <math>F[p]</math> è una tautologia, anche <math>F[X/p]</math> lo è.
# Ogni formula di una dimostrazione per <math>A</math> da <math>\Gamma</math> è soddisfatta da <math>\Gamma</math>.
 
La verifica che ''a'', ''b'' e ''c'' sono tautologie è banale.
 
Verifichiamo che MP è chiuso rispetto alla conseguenza logica. Supponiamo per assurdo che <math>\vDashGamma \models A</math> e <math>\vDashGamma \models A \to B</math>, ma <math>\Gamma \nvDash B</math>. Se <math>\Gamma \nvDash B</math>, allora esiste un modello <math>\mathcal{M_V}</math> tale che non<math>\mathcal{M_V} soddisfa\vDash \Gamma</math> e <math>\mathcal{M_V} \nvDash B</math>; ma <math>A</math> è unasoddisfatta tautologiada <math>\Gamma</math>, perciò è verificata in ogni modello, quindi anche in <math>\mathcal{M_V}</math>. Pertanto, <math>\mathcal{M_V} \models A</math> e <math>\mathcal{M_V} \nvDash B</math> e, per definizione di implicazione logica, <math>\mathcal{M_V} \nvDash A \to B</math>, dunque <math>\Gamma \nvDash A \to B</math>; contraddizione.
 
Per quanto riguarda la SU, sia <math>F[p]</math> una tautologia. Allora, <math>\vDash F[p]</math> per qualunque assegnazione booleana alle lettere proposizionali di <math>F[p]</math>, in particolare a <math>p</math>; dunque, per qualunque proposizione <math>X</math> possiamo porre <math>I_\mathcal{V}(p)=I_\mathcal{V}(X)</math>. Per il teorema del rimpiazzamento, <math>I_\mathcal{V}(F[p/p])=I_\mathcal{V}(F[X/p])</math>, da cui segue <math>\vDash F[X/p]</math>.
 
Dimostriamo ora il punto 3. Sia <math>A_1,...,A_n=A</math> una dimostrazione da <math>\Gamma</math> per <math>A</math>. Procediamo per induzione completa.
 
(''Passo base'') <math>\Gamma \vDash A_1</math> vale sse, per ogni modello <math>\mathcal{M_V}</math>, se <math>\mathcal{M_V} \vDash \Gamma</math> allora <math>\mathcal{M_V} \vDash A_1</math>. <math>A_1 \in \Gamma</math> oppure <math>A_1</math> è un assioma. Se <math>A_1 \in \Gamma</math>, allora abbiamo <math>\Gamma \vDash A_1</math> per definizione di modello; se <math>A_1</math> è un'istanza di assioma, allora, essendo SU chiuso rispetto alla conseguenza logica, <math>\vDash A_1</math>, dunque <math>\Gamma \models A_1</math>.
 
(''Passo induttivo'') Supponiamo vero per ogni <math>i<n</math> che <math>\Gamma \models A_i</math>. Se <math>A_n \in \Gamma</math> o <math>A_n</math> è un'istanza di assioma, allora, come sopra, <math>\Gamma \models A_n</math>. Se <math>A_n</math> è stato derivato mediante MP, lo si è ottenuto da <math>A_j</math>, <math>A_k=A_j \to A_n</math>, <math>j,k<n</math>, ma per ipotesi induttiva <math>\Gamma \models A_j</math> e <math>\Gamma \models A_k</math>, pertanto, essendo MP chiuso rispetto alla conseguenza logica, <math>\Gamma \models A_n</math>.
 
=== Teorema di completezza ===
Line 236 ⟶ 239:
 
:<math>\vDash A \to B</math> implica <math>\vdash A \to B</math>.
 
==== Dimostrazione ====
Scriviamo la tesi nella sua forma contrappositiva, ovvero:
 
:<math>\nvdash A \to B</math> implica <math>\nvDash A \to B</math>.
 
Mostriamo che, se <math>A \to B</math> non è un teorema, allora <math>A \to B</math> non è una tautologia, cioè non è una formula valida, vale a dire che <math>B</math> non segue logicamente da <math>A</math>. A tal fine basta costruire, analogamente a ciò che si fa nella [[Logica/Calcolo delle proposizioni/Dimostrazione del teorema di compattezza|dimostrazione del teorema di compattezza]], un insieme <math>\Delta</math> (deduttivamente chiuso e completo, cioè consistente e massimale) dal quale <math>A \to B</math> non è derivabile, cioè <math>\Delta \nvdash A \to B</math>. Mostreremo quindi che <math>\Delta</math> ha un modello che soddisfa <math>A</math> e non soddisfa <math>B</math>; dunque <math>\nvDash A \to B</math>.
 
Per costruire l'insieme <math>\Delta</math>, procediamo nel seguente modo. Enumeriamo tutte le formule del linguaggio:
 
:<math>A_0,A_1,A_2...</math>
 
Definiamo, ora, una sequenza di insiemi di formule, per induzione:
 
:<math>\Delta_0=\{A\};</math>
:<math>\Delta_{i+1} = \begin{cases}
\Delta_i \cup \{A_i\}, & \text{se }\Delta_i, A_i \nvdash B; \\
\Delta_i, & \text{altrimenti.}
\end{cases}</math>
 
per tutti gli <math>i>0</math>. Osserviamo innanzitutto che <math>\Delta_i \nvdash B</math>, per ogni <math>i</math>. Infatti, per induzione, abbiamo che
 
(''Passo base'') <math>\Delta_0 \nvdash B</math>, perché <math>\Delta_0=\{A\}</math> e, per ipotesi, <math>A \to B</math> non è un teorema.
 
(''Passo induttivo'') Per costruzione dei <math>\Delta_i</math>.
 
Sia ora
 
<math>\Delta = \bigcup_i \Delta_i</math>.
 
Osserviamo che
 
:1. Per costruzione, <math>A \in \Delta</math>.
:2. <math>\Delta \nvdash B</math>. Per dimostrare ciò, osserviamo innanzitutto che <math>B</math> non è un teorema; infatti, se lo fosse, avremmo <math>\vdash B</math> e, per monotonia, <math>A \vdash B</math>; quindi, per il teorema di deduzione, <math>\vdash A \to B</math>, contraddicendo l'ipotesi. Supponiamo dunque che <math>B</math> non sia un teorema, e che <math>\Delta \vdash B</math>; esiste quindi una derivazione <math>B_1,...,B_n=B</math> in <math>\Delta</math>, con qualche <math>B_j \in \Delta</math>. L'insieme di tali <math>B_j</math> è finito, quindi esiste un <math>\Delta_i</math> che li include tutti. Dunque <math>\Delta_i \vdash B</math>, contraddizione. Siccome c'è una proposizione che non deriva da <math>\Delta</math>, <math>\Delta</math> è consistente.
:3. <math>B \not\in \Delta</math>, per la proprietà di inclusione di <math>\vdash</math>.
:4. <math>\Delta</math> è deduttivamente chiuso, cioè, per ogni formula <math>F</math>
::<math>F \in \Delta</math> sse <math>\Delta \vdash F</math>. Se <math>F \in \Delta</math> allora <math>\Delta \vdash F</math> è la proprietà di inclusione.
:Ci rimane quindi da dimostrare che se <math>\Delta \vdash F</math> allora <math>F \in \Delta</math>.
:Sia <math>\Delta \vdash F</math>, e supponiamo per assurdo che <math>F \not\in \Delta</math>. Poiché l'enumerazione <math>A_0,A_1,A_2...</math> comprende tutte le formule, <math>F</math> sarà un <math>A_i</math>. Per ipotesi, <math>F=A_i \not\in \Delta</math>, dunque <math>F=A_i \not\in \Delta_{i+1}</math> e quindi, per costruzione, <math>\Delta_i, F \vdash B</math>. Per costruzione, <math>\Delta_i \subset \Delta</math> e, per ipotesi, <math>\Delta \vdash F</math>. Dunque, per taglio sulle premesse, abbiamo che <math>\Delta \vdash B</math>, contraddizione con il punto 2.
:5. Dimostriamo ora che l'insieme <math>\Delta</math> è massimale, ovvero, per ogni formula <math>F</math>
:<math>F \in \Delta</math> oppure <math>\neg F \in \Delta</math>.
:Sia <math>F \not\in \Delta</math>, e supponiamo per assurdo che <math>\neg F \not\in \Delta</math>. Allora, per qualche <math>i</math> e <math>j</math>: <math>\Delta_i, F \vdash B</math> e <math>\Delta_j, \neg F \vdash B</math>.
:<!-- Dobbiamo ora mostrare che {\displaystyle \Delta } è soddisfacibile. Per far questo, costruiamo un modello per esso. Definiamo il modello {\displaystyle {\mathcal {M_{V}}}} come:
 
{\displaystyle {\mathcal {M_{V}}}={\mathcal {P}}}
 
dove {\displaystyle {\mathcal {P}}} è l'insieme dei simboli proposizionali del linguaggio.
 
Dimostriamo ora, per induzione strutturale sulle formule, che per ogni formula {\displaystyle A} :
 
{\displaystyle A\in \Delta } sse {\displaystyle {\mathcal {M_{V}}}\models A} .
 
(Passo base) Per costruzione di {\displaystyle {\mathcal {M_{V}}}} .
 
(Passo induttivo) Sia {\displaystyle A=\neg B} . {\displaystyle {\mathcal {M_{V}}}\models \neg B} equivale a {\displaystyle {\mathcal {M_{V}}}\nvDash B} ; per ipotesi induttiva, {\displaystyle {\mathcal {M_{V}}}\nvDash B} sse {\displaystyle B\not \in \Delta } . Siccome {\displaystyle \Delta } è massimale, da {\displaystyle B\not \in \Delta } segue {\displaystyle \neg B\in \Delta } . Pertanto, {\displaystyle {\mathcal {M_{V}}}\models \neg B} sse {\displaystyle \neg B\in \Delta } , che è la tesi.
 
Sia {\displaystyle A=B\land C} . {\displaystyle {\mathcal {M_{V}}}\models B\land C} sse {\displaystyle I_{\mathcal {V}}(B\land C)=\mathrm {T} } sse {\displaystyle {\mathcal {Op}}_{\land }(I_{\mathcal {V}}(B),I_{\mathcal {V}}(C))=\mathrm {T} } sse {\displaystyle I_{\mathcal {V}}(B)=\mathrm {T} } e {\displaystyle I_{\mathcal {V}}(C)=\mathrm {T} } sse {\displaystyle {\mathcal {M_{V}}}\models B} e {\displaystyle {\mathcal {M_{V}}}\models C} ; per ipotesi induttiva, abbiamo {\displaystyle {\mathcal {M_{V}}}\models B} sse {\displaystyle B\in \Delta } e {\displaystyle {\mathcal {M_{V}}}\models C} sse {\displaystyle C\in \Delta } . Quindi {\displaystyle B,C\in \Delta } , ovvero {\displaystyle B\land C\in \Delta } , che è la tesi.
 
Sia {\displaystyle A=B\lor C} . {\displaystyle {\mathcal {M_{V}}}\models B\lor C} sse {\displaystyle I_{\mathcal {V}}(B\lor C)=\mathrm {T} } sse {\displaystyle {\mathcal {Op}}_{\lor }(I_{\mathcal {V}}(B),I_{\mathcal {V}}(C))=\mathrm {T} } sse {\displaystyle I_{\mathcal {V}}(B)=\mathrm {T} } o {\displaystyle I_{\mathcal {V}}(C)=\mathrm {T} } sse {\displaystyle {\mathcal {M_{V}}}\models B} o {\displaystyle {\mathcal {M_{V}}}\models C} ; per ipotesi induttiva, abbiamo {\displaystyle {\mathcal {M_{V}}}\models B} sse {\displaystyle B\in \Delta } o {\displaystyle {\mathcal {M_{V}}}\models C} sse {\displaystyle C\in \Delta } . Quindi {\displaystyle B\in \Delta } o {\displaystyle C\in \Delta } , ovvero {\displaystyle B\lor C\in \Delta } , che è la tesi.
 
Sia {\displaystyle A=B\to C} . {\displaystyle {\mathcal {M_{V}}}\models B\to C} sse {\displaystyle I_{\mathcal {V}}(B\to C)=\mathrm {T} } sse {\displaystyle {\mathcal {Op}}_{\to }(I_{\mathcal {V}}(B),I_{\mathcal {V}}(C))=\mathrm {T} } sse {\displaystyle I_{\mathcal {V}}(B)=\mathrm {F} } o {\displaystyle I_{\mathcal {V}}(C)=\mathrm {T} } sse {\displaystyle {\mathcal {M_{V}}}\nvDash B} o {\displaystyle {\mathcal {M_{V}}}\models C} ; per ipotesi induttiva, abbiamo {\displaystyle {\mathcal {M_{V}}}\nvDash B} sse {\displaystyle B\not \in \Delta } o {\displaystyle {\mathcal {M_{V}}}\models C} sse {\displaystyle C\in \Delta } . Siccome {\displaystyle \Delta } è massimale, da {\displaystyle B\not \in \Delta } segue {\displaystyle \neg B\in \Delta } . Quindi {\displaystyle \neg B\in \Delta } o {\displaystyle C\in \Delta } , ovvero {\displaystyle B\to C\in \Delta } , che è la tesi.
 
Sia {\displaystyle A=B\leftrightarrow C} . {\displaystyle {\mathcal {M_{V}}}\models B\leftrightarrow C} sse {\displaystyle I_{\mathcal {V}}(B\leftrightarrow C)=\mathrm {T} } sse {\displaystyle {\mathcal {Op}}_{\leftrightarrow }(I_{\mathcal {V}}(B),I_{\mathcal {V}}(C))=\mathrm {T} } sse {\displaystyle I_{\mathcal {V}}(B)=\mathrm {T} } e {\displaystyle I_{\mathcal {V}}(C)=\mathrm {T} } , o {\displaystyle I_{\mathcal {V}}(B)=\mathrm {F} } e {\displaystyle I_{\mathcal {V}}(C)=\mathrm {F} } , sse {\displaystyle {\mathcal {M_{V}}}\models B} e {\displaystyle {\mathcal {M_{V}}}\models C} , o {\displaystyle {\mathcal {M_{V}}}\nvDash B} e {\displaystyle {\mathcal {M_{V}}}\nvDash C} ; per ipotesi induttiva, abbiamo {\displaystyle {\mathcal {M_{V}}}\models B} sse {\displaystyle B\in \Delta } e {\displaystyle {\mathcal {M_{V}}}\models C} sse {\displaystyle C\in \Delta } , o {\displaystyle {\mathcal {M_{V}}}\nvDash B} sse {\displaystyle B\not \in \Delta } e {\displaystyle {\mathcal {M_{V}}}\nvDash C} sse {\displaystyle C\not \in \Delta } . Quindi {\displaystyle B,C\in \Delta } o {\displaystyle B,C\not \in \Delta } , ovvero {\displaystyle B\leftrightarrow C\in \Delta } , che è la tesi.
 
Abbiamo quindi mostrato che {\displaystyle {\mathcal {M_{V}}}} è un modello per {\displaystyle \Delta } ; siccome {\displaystyle \Gamma \subseteq \Delta } , abbiamo che {\displaystyle {\mathcal {M_{V}}}\models \Gamma } , ovvero {\displaystyle \Gamma } è soddisfacibile. -->
 
== Regole derivate ==
 
Le seguenti sono regole derivate dal MP e gli schemi di assioma, per permettere di utilizzare agevolmente il sistema di Hilbert. È possibile dimostrare ognuna di esse attraverso il teorema di completezza.
 
==== Modus Tollens ====
 
<math>
\neg B,\quad A \to B \over \neg A
</math>
 
''Dimostrazione''
 
Sia <math>\Gamma</math> un insieme di formule. Se <math>\Gamma \vdash \neg B</math> e <math>\Gamma \vdash A \to B</math>, allora <math>\Gamma \vdash \neg A</math>.
 
Se <math>\Gamma</math> non è consistente, la tesi è banalmente dimostrata. Supponiamo allora che <math>\Gamma</math> sia consistente.
 
Per il teorema di deduzione, da <math>\Gamma \vdash A \to B</math> si ha che <math>\Gamma, A \vdash B</math>; ma, per monotonia, da <math>\Gamma \vdash \neg B</math> ricaviamo <math>\Gamma, A \vdash \neg B</math>. Quindi, l'insieme <math>\Gamma \cup \{A\}</math> è inconsistente, cioè è insoddisfacibile, ragion per cui <math>\Gamma \models \neg A</math>. Dunque, per il teorema di completezza, <math>\Gamma \vdash \neg A</math>.
 
====== Regola di deduzione ======
Line 331 ⟶ 255:
\neg B \to \neg A \over A \to B
</math>
 
Deriva direttamente dallo schema ''c''.
 
====== Regola di transitività ======
Line 349 ⟶ 275:
''Dimostrazione''
 
SiaEssendo <math> \Gammaneg A \to (A \to B) </math> un insiemeteorema, diper formule.il Essendoteorema chedi <math>\Gammadeduzione \vdashsi A</math>ha eche <math>\Gamma \vdash \neg A</math>, <math>\Gamma</math> è inconsistente, dunque <math>\GammaA \vdash B</math> per ogni formula <math>B</math>.
 
====== RegolaConsequentia della doppia negazionemirabilis ======
<math>
\negvdash (\neg A \overto A) \to A
</math>
 
''Dimostrazione''
====== Consequentia mirabilis ======
 
<math>
# <math>
\neg A \to A
</math>: ipotesi;
# <math> \vdash \neg A \to (A \to \neg (\neg A \to A)) </math>: SU sul teorema dello Pseudo-Scoto;
# <math> \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))) </math>: SU in ''b'';
# <math> \vdash (\neg A \to A) \to (\neg A \to \neg (\neg A \to A)) </math>: MP tra 2 e 3;
# <math> \neg A \to \neg (\neg A \to A) </math>: MP tra 1 e 4;
# <math> \vdash (\neg A \to \neg (\neg A \to A)) \to ((\neg A \to A) \to A) </math>: SU in ''c'';
# <math> (\neg A \to A) \to A </math>: MP tra 5 e 6;
# <math> A </math>: MP tra 1 e 7.
 
Quindi, <math>
\neg A \to A \vdash A
</math>. Dunque, per il teorema di deduzione, <math>
\vdash (\neg A \to A) \to A
</math>.
 
====== Eliminazione della doppia negazione ======
<math>
\neg\neg A \over A
</math>
 
''Dimostrazione''
 
Essendo# <math>
A \toneg\neg A
</math>: ipotesi;
</math> un teorema, per SU abbiamo che <math>
# <math> \vdash \neg\neg A \to (\neg A \to A) </math>: SU sul teorema dello Pseudo-Scoto;
# </math>. Per\neg SUA di\to A </math>: MP tra 1 e 2;
# <math>
B
</math> con <math>
A
</math> sullo schema ''c'', si ha che <math>
\vdash (\neg A \to \neg A) \to ((\neg A \to A) \to A)
</math>. Dunque, per MP di <math>
\vdash \neg A \to \neg A
</math>, abbiamo <math>
\vdash (\neg A \to A) \to A
</math>: Consequentia mirabilis;
# <math> A </math>: MP tra 3 e 4.
 
Dunque, <math>
\neg\neg A \vdash A
</math>.
 
==== Introduzione della doppia negazione ====
<math>
A \over \neg\neg A
</math>
 
''Dimostrazione''
 
# <math>
\neg\neg A \vdash A
</math>: eliminazione della doppia negazione;
# <math>
\vdash \neg\neg A \to A
</math>: teorema di deduzione su 1;
# <math>
\vdash \neg\neg\neg A \to \neg A
</math>: SU in 2 con <math>
\neg A
</math> al posto di <math> A </math>;
# <math>
\vdash (\neg\neg\neg A \to \neg A) \to (A \to \neg\neg A)
</math>: SU in ''c'';
# <math>
\vdash A \to \neg\neg A
</math>: MP tra 3 e 4;
# <math>
A \vdash \neg\neg A
</math>: teorema di deduzione su 5;
 
==== Modus Tollens ====
 
<math>
\neg B,\quad A \to B \over \neg A
</math>
 
== Esempi di dimostrazioni ==
 
=== Riflessività dell'implicazione ===
Dimostriamo che <math> \phi \to \phi </math>.
Dimostriamo che <math> \vdash A \to A </math>.
 
# <math>
(\phivdash (A \to ((\psiB \to \phiA) \to \phiA)) \to ((\phiA \to (\psiB \to \phiA)) \to (\phiA \to \phiA))
</math>: SU nellosullo schema ''b'' con <math>\phiA</math> al posto di <math>A\phi</math>, e <math>C\chi</math> e, <math>\psiB \to \phiA</math> al posto di <math>B\psi</math>;
# <math>
\phivdash A \to ((\psiB \to \phiA)\to \phiA)
</math>: SU in ''a'' con <math>\phiA</math> al posto di <math>A\phi</math> e <math>\psiB \to \phiA</math> al posto di <math>B\psi</math>;
# <math>
(\phivdash (A \to (\psiB \to \phiA)) \to (\phiA \to \phiA)
</math>: MP tra 1 e 2;
# <math>
(\phivdash (A \to (\psiB \to \phiA))
</math>: SU in ''a'' con <math>\phiA</math> al posto di <math>A\phi</math> e <math>\psiB</math> al posto di <math>B\psi</math>;
# <math> \vdash A \to A </math>: MP tra 3 e 4.
# <math>
 
\phi \to \phi
=== Sillogismo ipotetico ===
</math>: MP tra 3 e 4.
Dimostriamo che <math> A \to B, B \to C \vdash A \to C </math>.
 
# <math>A</math>: ipotesi;
# <math>A \to B</math>: ipotesi;
# <math>B</math>: MP tra 1 e 2;
# <math>B \to C</math>: ipotesi;
# <math>C</math>: MP tra 3 e 4.
 
Così abbiamo dimostrato che <math> A, A \to B, B \to C \vdash C </math>.
 
Applicando il teorema di deduzione (se <math> A \vdash C</math> allora <math> \vdash A \to C</math>), otteniamo il risultato voluto, eliminando <math> A</math> dalle ipotesi che abbiamo utilizzato.
Dimostriamo che <math> \phi \to \psi, \psi \to \omega \vdash \phi \to \omega </math>.
 
=== Teorema dello Pseudo-Scoto ===
# <math>\phi</math>: ipotesi;
#Dimostriamo che <math> \phivdash \neg A \to (A \psito B) </math>: ipotesi;.
# <math>\psi</math>: MP tra 1 e 2;
# <math>\psi \to \omega</math>: ipotesi;
# <math>\omega</math>: MP tra 3 e 4.
 
# <math>\neg A</math>: ipotesi;
Così abbiamo dimostrato che <math> \phi, \phi \to \psi, \psi \to \omega \vdash \omega </math>.
# <math> \vdash \neg A \to (\neg B \to \neg A) </math>: SU in ''a'';
# <math> \neg B \to \neg A </math>: MP tra 1 e 2;
# <math> \vdash (\neg B \to \neg A) \to (A \to B) </math>: SU in ''c'';
# <math> A \to B </math>: MP tra 3 e 4.
 
ApplicandoAbbiamo ildimostrato teorema di deduzione (seche <math> \phineg \vdash \omega</math> allora <math>A \vdash \phiA \to \omegaB </math>). Dunque, otteniamoper il risultatoteorema voluto,di eliminandodeduzione, <math> \phi</math>vdash dalle\neg ipotesiA che\to abbiamo(A utilizzato\to B) </math>.
 
{{avanzamento|75%}}
Estratto da "https://it.wikibooks.org/wiki/Logica_matematica/Calcolo_delle_proposizioni/Sistema_di_Hilbert"