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 108:
 
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 <math>\vdash</math>, abbiamo che, se <math>\Gamma \vdash A</math>, allora esiste un insieme finito <math>\Gamma_0 \subseteq \Gamma</math> tale che <math>\Gamma_0 \vdash A</math>. Siccome <math>\Gamma_0</math> è finito, sarà del tipo <math>\{A_1,...,A_n\}</math>, o equivalentemente <math>\{A_1 \and ... \and A_n\}</math>, quindi <math>\Gamma \vdash A</math> implica <math>\Gamma_0 \vdash A</math>, che equivale a <math>A_1 \and ... \and A_n \vdash A</math> e <math>A_1,...,A_n \vdash A</math>. Per il teorema di deduzione, otteniamo <math>\vdash (A_1 \and ... \and A_n) \to A</math> e <math>\vdash A_1 \to(... \to (A_n \to A)...)</math>.
 
== Consistenza ==▼
Introduciamo ora la nozione di ''consistenza''.▼
 
==== Insieme di formule consistente ====▼
{{Definizione|▼
Un insieme di formule proposizionali <math>\Gamma</math> è ''consistente'' sse è verificata una delle seguenti proprietà:▼
 
# non esiste una proposizione <math>A</math> tale che <math>\Gamma \vdash A</math> e <math>\Gamma \vdash \neg A</math>;▼
# esiste una proposizione <math>A</math> tale che <math>\Gamma \nvdash A</math>.▼
}}Si può dimostrare che le due formulazioni sono equivalenti.▼
 
(<math>\Rightarrow</math>) Se non esiste una proposizione <math>A</math> tale che <math>\Gamma \vdash A</math> e <math>\Gamma \vdash \neg A</math>, allora si ha che <math>\Gamma \nvdash A</math> oppure <math>\Gamma \nvdash \neg A</math> per ogni proposizione <math>A</math>, dunque esiste una proposizione <math> B</math> tale che <math>\Gamma \nvdash B</math>.▼
 
(<math>\Leftarrow</math>) Viceversa, supponiamo che esista una proposizione <math>A</math> tale che <math>\Gamma \vdash A</math> e <math>\Gamma \vdash \neg A</math>, e che non esista 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 \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 A \to (\neg A \to B)</math>. Dunque, <math>A, \neg A \vdash B</math> sse <math>\vdash A \to (\neg A \to B)</math>.▼
 
Essendo che <math>\vDash A \to (\neg A \to B)</math>, allora, per il [[Logica/Calcolo delle proposizioni/Sistema di Hilbert#Teorema di completezza|teorema di completezza]], è vero che <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>.▼
 
==== Insieme di formule completo ====▼
{{Definizione|▼
Un insieme di formule <math>\Gamma</math> si dice ''consistente e massimale'' o ''completo'' se, per ogni formula <math>A \in \mathcal{L}</math>, si verifica una e una sola delle seguenti relazioni:▼
 
:<math>\Gamma \vdash A</math> oppure <math>\Gamma \vdash \neg A</math>.▼
}}▼
 
Notare che la nozione di insieme consistente e massimale è analoga a quella di [[Logica/Calcolo delle proposizioni/Dimostrazione del teorema di compattezza#Insieme di formule massimale|insieme massimale]] soddisfacibile.▼
 
== Correttezza e completezza ==
Line 177 ⟶ 207:
:<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 [[Logica/Calcolo delle proposizioni/Sistema di Hilbert#Insieme di formule completo|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:
Line 186 ⟶ 216:
 
:<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>
<!--
Sia <math>\Delta = \bigcup_i \Delta_i</math>. Osserviamo innanzitutto che <math>\Gamma \subseteq \Delta</math>, per costruzione. Osserviamo inoltre che <math>\Delta</math> è massimale, cioè, per ogni formula <math>A</math>, <math>A</math> o la sua negazione appartengono a <math>\Delta</math>. Infatti, siccome l'enumerazione delle formule è completa, per costruzione dei <math>\Delta_i</math>, presa una qualunque <math>A</math>, esisterà un <math>i</math> per cui <math>A=A_i</math>, quindi <math>A \in \Delta_i \subseteq \Delta</math> oppure <math>\neg A \in \Delta_i \subseteq \Delta</math>. Osserviamo anche che ciascun <math>\Delta_i</math> è finitamente soddisfacibile (per induzione: <math>\Delta_0=\Gamma</math> è finitamente soddisfacibile; il passo induttivo è giustificato dal lemma 2). Quindi, <math>\Delta</math> è finitamente soddisfacibile, in quanto ogni sottoinsieme finito di <math>\Delta</math> è contenuto in qualche <math>\Delta_i</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
Dobbiamo ora mostrare che <math>\Delta</math> è soddisfacibile. Per far questo, costruiamo un modello per esso. Definiamo il modello <math>\mathcal{M_V}</math> come:▼
 
(''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.
<math>\mathcal{M_V}=\mathcal{P}</math>▼
 
(''Passo baseinduttivo'') Per costruzione didei <math>\mathcal{M_V}Delta_i</math>.▼
dove <math>\mathcal{P}</math> è l'insieme dei simboli proposizionali del linguaggio.▼
 
Sia ora
Dimostriamo ora, per induzione strutturale sulle formule, che per ogni formula <math>A</math>:▼
 
<math>A \in \Delta</math> sse= <math>\mathcal{M_V}bigcup_i \models ADelta_i</math>.
 
Osserviamo che
▲(''Passo base'') Per costruzione di <math>\mathcal{M_V}</math>.
 
Per costruzione, <math>A \in \Delta</math>.
(''Passo Induttivo'') Sia <math>A=\neg B</math>. <math>\mathcal{M_V} \models \neg B</math> equivale a <math>\mathcal{M_V} \nvDash B</math>; per ipotesi induttiva, <math>\mathcal{M_V} \nvDash B</math> sse <math>B \not\in \Delta</math>. Siccome <math>\Delta</math> è massimale, da <math>B \not\in \Delta</math> segue <math>\neg B \in \Delta</math>. Pertanto, <math>\mathcal{M_V} \models \neg B</math> sse <math>\neg B \in \Delta</math>, che è la tesi.▼
 
Sia <math>A=B\Delta \andnvdash CB</math>. <math>\mathcal{M_V}Per \modelsdimostrare Bciò, \andosserviamo C</math>innanzitutto sseche <math>I_\mathcal{V}(B \and C)=\mathrm{T}</math> ssenon <math>\mathcal{Op}_\and(I_\mathcal{V}(B)è un teorema; infatti, I_\mathcal{V}(C))=\mathrm{T}</math>se sselo fosse, avremmo <math>I_\mathcal{V}(vdash B)=\mathrm{T}</math> e, per monotonia, <math>I_\mathcal{V}(C)=A \mathrm{T}vdash B</math>; ssequindi, per il teorema di deduzione, <math>\mathcal{M_V}vdash A \modelsto B</math>, econtraddicendo l'ipotesi. Supponiamo dunque che <math>\mathcal{M_V} \models CB</math>; pernon ipotesisia induttivaun teorema, abbiamoe che <math>\mathcal{M_V}Delta \modelsvdash B</math>; esiste quindi una ssederivazione <math>B_1,...,B_n=B \in \Delta</math> ein <math>\mathcal{M_V} \models CDelta</math>, ssecon qualche <math>CB_j \in \Delta</math>. QuindiL'insieme di tali <math>BB_j</math> è finito,C \inquindi esiste un <math>\DeltaDelta_i</math>, ovveroche li include tutti. Dunque <math>B\Delta_i \andvdash CB</math>, \incontraddizione. Siccome c'è una proposizione che non deriva da <math>\Delta</math>, che<math>\Delta</math> è la tesiconsistente.
 
<math>B \not\in \Delta</math>, per la proprietà di inclusione di <math>\vdash</math>.
Sia <math>A=B \or C</math>. <math>\mathcal{M_V} \models B \or C</math> sse <math>I_\mathcal{V}(B \or C)=\mathrm{T}</math> sse <math>\mathcal{Op}_\or(I_\mathcal{V}(B), I_\mathcal{V}(C))=\mathrm{T}</math> sse <math>I_\mathcal{V}(B)=\mathrm{T}</math> o <math>I_\mathcal{V}(C)=\mathrm{T}</math> sse <math>\mathcal{M_V} \models B</math> o <math>\mathcal{M_V} \models C</math>; per ipotesi induttiva, abbiamo <math>\mathcal{M_V} \models B</math> sse <math>B \in \Delta</math> o <math>\mathcal{M_V} \models C</math> sse <math>C \in \Delta</math>. Quindi <math>B \in \Delta</math> o <math>C \in \Delta</math>, ovvero <math>B \or C \in \Delta</math>, che è la tesi.▼
 
<math>\Delta</math> è deduttivamente chiuso, cioè, per ogni formula <math>F</math>
Sia <math>A=B \to C</math>. <math>\mathcal{M_V} \models B \to C</math> sse <math>I_\mathcal{V}(B \to C)=\mathrm{T}</math> sse <math>\mathcal{Op}_\to(I_\mathcal{V}(B), I_\mathcal{V}(C))=\mathrm{T}</math> sse <math>I_\mathcal{V}(B)=\mathrm{F}</math> o <math>I_\mathcal{V}(C)=\mathrm{T}</math> sse <math>\mathcal{M_V} \nvDash B</math> o <math>\mathcal{M_V} \models C</math>; per ipotesi induttiva, abbiamo <math>\mathcal{M_V} \nvDash B</math> sse <math>B \not\in \Delta</math> o <math>\mathcal{M_V} \models C</math> sse <math>C \in \Delta</math>. Siccome <math>\Delta</math> è massimale, da <math>B \not\in \Delta</math> segue <math>\neg B \in \Delta</math>. Quindi <math>\neg B \in \Delta</math> o <math>C \in \Delta</math>, ovvero <math>B \to C \in \Delta</math>, che è la tesi.▼
 
▲Dobbiamo<math>F ora\in mostrare\Delta</math> chesse <math>\Delta \vdash F</math>.<!-- Dobbiamo ora mostrare che {\displaystyle \Delta } è soddisfacibile. Per far questo, costruiamo un modello per esso. Definiamo il modello <math>{\displaystyle {\mathcal {M_VM_{V}</math>}}} come:
Sia <math>A=B \leftrightarrow C</math>. <math>\mathcal{M_V} \models B \leftrightarrow C</math> sse <math>I_\mathcal{V}(B \leftrightarrow C)=\mathrm{T}</math> sse <math>\mathcal{Op}_\leftrightarrow (I_\mathcal{V}(B), I_\mathcal{V}(C))=\mathrm{T}</math> sse <math>I_\mathcal{V}(B)=\mathrm{T}</math> e <math>I_\mathcal{V}(C)=\mathrm{T}</math>, o <math>I_\mathcal{V}(B)=\mathrm{F}</math> e <math>I_\mathcal{V}(C)=\mathrm{F}</math>, sse <math>\mathcal{M_V} \models B</math> e <math>\mathcal{M_V} \models C</math>, o <math>\mathcal{M_V} \nvDash B</math> e <math>\mathcal{M_V} \nvDash C</math>; per ipotesi induttiva, abbiamo <math>\mathcal{M_V} \models B</math> sse <math>B \in \Delta</math> e <math>\mathcal{M_V} \models C</math> sse <math>C \in \Delta</math>, o <math>\mathcal{M_V} \nvDash B</math> sse <math>B \not\in \Delta</math> e <math>\mathcal{M_V} \nvDash C</math> sse <math>C \not\in \Delta</math>. Quindi <math>B,C \in \Delta</math> o <math>B,C \not\in \Delta</math>, ovvero <math>B \leftrightarrow C \in \Delta</math>, che è la tesi.▼
 
▲<math>{\displaystyle {\mathcal {M_VM_{V}}}={\mathcal {P}</math>}}
Abbiamo quindi mostrato che <math>\mathcal{M_V}</math> è un modello per <math>\Delta</math>; siccome <math>\Gamma \subseteq \Delta</math>, abbiamo che <math>\mathcal{M_V} \models \Gamma</math>, ovvero <math>\Gamma</math> è soddisfacibile.▼
-->
 
▲dove <math>{\displaystyle {\mathcal {P}</math>}} è l'insieme dei simboli proposizionali del linguaggio.
▲== Consistenza ==
▲Introduciamo ora la nozione di ''consistenza''.
 
▲Dimostriamo ora, per induzione strutturale sulle formule, che per ogni formula <math>{\displaystyle A</math>} :
▲==== Insieme di formule consistente ====
▲{{Definizione|
▲Un insieme di formule proposizionali <math>\Gamma</math> è ''consistente'' sse è verificata una delle seguenti proprietà:
 
{\displaystyle A\in \Delta } sse {\displaystyle {\mathcal {M_{V}}}\models A} .
▲# non esiste una proposizione <math>A</math> tale che <math>\Gamma \vdash A</math> e <math>\Gamma \vdash \neg A</math>;
▲# esiste una proposizione <math>A</math> tale che <math>\Gamma \nvdash A</math>.
▲}}Si può dimostrare che le due formulazioni sono equivalenti.
 
(Passo base) Per costruzione di {\displaystyle {\mathcal {M_{V}}}} .
▲(<math>\Rightarrow</math>) Se non esiste una proposizione <math>A</math> tale che <math>\Gamma \vdash A</math> e <math>\Gamma \vdash \neg A</math>, allora si ha che <math>\Gamma \nvdash A</math> oppure <math>\Gamma \nvdash \neg A</math> per ogni proposizione <math>A</math>, dunque esiste una proposizione <math> B</math> tale che <math>\Gamma \nvdash B</math>.
 
▲(''Passo Induttivo''induttivo) Sia <math>{\displaystyle A=\neg B</math>} . <math>{\displaystyle {\mathcal {M_{M_VV}}} \models \neg B</math>} equivale a <math>{\displaystyle {\mathcal {M_VM_{V}}} \nvDash B</math>} ; per ipotesi induttiva, <math>{\displaystyle {\mathcal {M_{M_VV}}} \nvDash B</math>} sse <math>B{\displaystyle B\not \in \Delta</math> } . Siccome <math>{\displaystyle \Delta</math> } è massimale, da <math>B{\displaystyle B\not \in \Delta</math> } segue <math>{\displaystyle \neg B \in \Delta</math> } . Pertanto, <math>{\displaystyle {\mathcal {M_VM_{V}}} \models \neg B</math>} sse <math>{\displaystyle \neg B \in \Delta</math> } , che è la tesi.
▲(<math>\Leftarrow</math>) Viceversa, supponiamo che esista una proposizione <math>A</math> tale che <math>\Gamma \vdash A</math> e <math>\Gamma \vdash \neg A</math>, e che non esista 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 \vdash B</math> per ogni formula <math> B</math>, allora, per taglio sulle premesse, si ha che <math>\Gamma \vdash B</math>.
 
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.
▲Per il teorema di deduzione, abbiamo che <math>\vdash A \to (\neg A \to B)</math>. Dunque, <math>A, \neg A \vdash B</math> sse <math>\vdash A \to (\neg A \to B)</math>.
 
▲Sia <math>{\displaystyle A=B \orlor C</math>} . <math>{\displaystyle {\mathcal {M_VM_{V}}} \models B \orlor C</math>} sse <math>{\displaystyle I_{\mathcal {V}}(B \orlor C)=\mathrm {T}</math> } sse <math>{\displaystyle {\mathcal {Op}}_{\orlor }(I_{\mathcal {V}}(B), I_{\mathcal {V}}(C))=\mathrm {T}</math> } sse <math>{\displaystyle I_{\mathcal {V}}(B)=\mathrm {T}</math> } o <math>{\displaystyle I_{\mathcal {V}}(C)=\mathrm {T}</math> } sse <math>{\displaystyle {\mathcal {M_VM_{V}}} \models B</math>} o <math>{\displaystyle {\mathcal {M_VM_{V}}} \models C</math>} ; per ipotesi induttiva, abbiamo <math>{\displaystyle {\mathcal {M_VM_{V}}} \models B</math>} sse <math>B{\displaystyle B\in \Delta</math> } o <math>{\displaystyle {\mathcal {M_VM_{V}}} \models C</math>} sse <math>C{\displaystyle C\in \Delta</math> } . Quindi <math>B{\displaystyle B\in \Delta</math> } o <math>C{\displaystyle C\in \Delta</math> } , ovvero <math>B{\displaystyle B\orlor C \in \Delta</math> } , che è la tesi.
▲Essendo che <math>\vDash A \to (\neg A \to B)</math>, allora, per il [[Logica/Calcolo delle proposizioni/Sistema di Hilbert#Teorema di completezza|teorema di completezza]], è vero che <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>.
 
▲Sia <math>{\displaystyle A=B \to C</math>} . <math>{\displaystyle {\mathcal {M_VM_{V}}} \models B \to C</math>} sse <math>{\displaystyle I_{\mathcal {V}}(B \to C)=\mathrm {T}</math> } sse <math>{\displaystyle {\mathcal {Op}}_{\to }(I_{\mathcal {V}}(B), I_{\mathcal {V}}(C))=\mathrm {T}</math> } sse <math>{\displaystyle I_{\mathcal {V}}(B)=\mathrm {F}</math> } o <math>{\displaystyle I_{\mathcal {V}}(C)=\mathrm {T}</math> } sse <math>{\displaystyle {\mathcal {M_VM_{V}}} \nvDash B</math>} o <math>{\displaystyle {\mathcal {M_VM_{V}}} \models C</math>} ; per ipotesi induttiva, abbiamo <math>{\displaystyle {\mathcal {M_VM_{V}}} \nvDash B</math>} sse <math>B{\displaystyle B\not \in \Delta</math> } o <math>{\displaystyle {\mathcal {M_VM_{V}}} \models C</math>} sse <math>C{\displaystyle C\in \Delta</math> } . Siccome <math>{\displaystyle \Delta</math> } è massimale, da <math>B{\displaystyle B\not \in \Delta</math> } segue <math>{\displaystyle \neg B \in \Delta</math> } . Quindi <math>{\displaystyle \neg B \in \Delta</math> } o <math>C{\displaystyle C\in \Delta</math> } , ovvero <math>B{\displaystyle B\to C \in \Delta</math> } , che è la tesi.
▲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>.
 
▲Sia <math>{\displaystyle A=B \leftrightarrow C</math>} . <math>{\displaystyle {\mathcal {M_VM_{V}}} \models B \leftrightarrow C</math>} sse <math>{\displaystyle I_{\mathcal {V}}(B \leftrightarrow C)=\mathrm {T}</math> } sse <math>{\displaystyle {\mathcal {Op}}_{\leftrightarrow }(I_{\mathcal {V}}(B), I_{\mathcal {V}}(C))=\mathrm {T}</math> } sse <math>{\displaystyle I_{\mathcal {V}}(B)=\mathrm {T}</math> } e <math>{\displaystyle I_{\mathcal {V}}(C)=\mathrm {T}</math> } , o <math>{\displaystyle I_{\mathcal {V}}(B)=\mathrm {F}</math> } e <math>{\displaystyle I_{\mathcal {V}}(C)=\mathrm {F}</math> } , sse <math>{\displaystyle {\mathcal {M_VM_{V}}} \models B</math>} e <math>{\displaystyle {\mathcal {M_VM_{V}}} \models C</math>} , o <math>{\displaystyle {\mathcal {M_VM_{V}}} \nvDash B</math>} e <math>{\displaystyle {\mathcal {M_VM_{V}}} \nvDash C</math>} ; per ipotesi induttiva, abbiamo <math>{\displaystyle {\mathcal {M_VM_{V}}} \models B</math>} sse <math>B{\displaystyle B\in \Delta</math> } e <math>{\displaystyle {\mathcal {M_VM_{V}}} \models C</math>} sse <math>C{\displaystyle C\in \Delta</math> } , o <math>{\displaystyle {\mathcal {M_VM_{V}}} \nvDash B</math>} sse <math>B{\displaystyle B\not \in \Delta</math> } e <math>{\displaystyle {\mathcal {M_VM_{V}}} \nvDash C</math>} sse <math>C{\displaystyle C\not \in \Delta</math> } . Quindi <math>{\displaystyle B,C \in \Delta</math> } o <math>{\displaystyle B,C \not \in \Delta</math> } , ovvero <math>B{\displaystyle B\leftrightarrow C \in \Delta</math> } , che è la tesi.
▲==== Insieme di formule completo ====
▲{{Definizione|
▲Un insieme di formule <math>\Gamma</math> si dice ''consistente e massimale'' o ''completo'' se, per ogni formula <math>A \in \mathcal{L}</math>, si verifica una e una sola delle seguenti relazioni:
 
▲Abbiamo quindi mostrato che <math>{\displaystyle {\mathcal {M_VM_{V}</math>}}} è un modello per <math>{\displaystyle \Delta</math> } ; siccome <math>{\displaystyle \Gamma \subseteq \Delta</math> } , abbiamo che <math>{\displaystyle {\mathcal {M_VM_{V}}} \models \Gamma</math> } , ovvero <math>{\displaystyle \Gamma</math> } è soddisfacibile. -->
▲:<math>\Gamma \vdash A</math> oppure <math>\Gamma \vdash \neg A</math>.
▲}}
 
▲Notare che la nozione di insieme consistente e massimale è analoga a quella di [[Logica/Calcolo delle proposizioni/Dimostrazione del teorema di compattezza#Insieme di formule massimale|insieme massimale]] soddisfacibile.
 
== Esempi di dimostrazioni ==
Estratto da "https://it.wikibooks.org/wiki/Logica_matematica/Calcolo_delle_proposizioni/Sistema_di_Hilbert"