Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
Riga 155:
=== Teorema di completezza ===
:<math>\vDash A \to B</math> implica <math>\vdash A \to B</math>.▼
Prima di dimostrare il teorema di completezza, diamo alcune utili definizioni.
Line 170 ⟶ 168:
}}
==== Enunciato ====
▲:<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 [[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:
<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>
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>.
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:
<math>\mathcal{M_V}=\mathcal{P}</math>
dove <math>\mathcal{P}</math> è l'insieme dei simboli proposizionali del linguaggio.
Dimostriamo ora, per induzione strutturale sulle formule, che per ogni formula <math>A</math>:
<math>A \in \Delta</math> sse <math>\mathcal{M_V} \models A</math>.
(''Passo base'') Per costruzione di <math>\mathcal{M_V}</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 \and C</math>. <math>\mathcal{M_V} \models B \and C</math> sse <math>I_\mathcal{V}(B \and C)=\mathrm{T}</math> sse <math>\mathcal{Op}_\and(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> sse <math>\mathcal{M_V} \models B</math> e <math>\mathcal{M_V} \models 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>. Quindi <math>B,C \in \Delta</math>, ovvero <math>B \and C \in \Delta</math>, che è la tesi.
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.
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.
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.
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.
== Consistenza ==
Introduciamo ora la nozione di ''consistenza''.
| |||