Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
Riga 223:
=== Teorema di completezza ===
Prima di dimostrare il teorema di completezza, diamo alcune utili definizioni.▼
:<math>\Gamma \vDash A</math> implica <math>\Gamma \vdash A</math>.▼
==== Definizioni ====▼
▲
Sia <math>\Gamma</math>un insieme di formule e sia <math>A</math> una formula. <math>\Gamma \vdash A</math>sse <math>\Gamma \cup \{\neg A\}</math> è inconsistente.
''Dimostrazione''
(<math>\Rightarrow</math>) Supponiamo che <math>\Gamma \vdash A</math>. Allora, per monotonia, <math>\Gamma, \neg A \vdash A</math>. Dal momento che, per inclusione, <math>\Gamma, \neg A \vdash \neg A</math>, <math>\Gamma \cup \{\neg A\}</math> è inconsistente.
==== Enunciato ====▼
(<math>\Leftarrow</math>) Supponiamo che <math>\Gamma \cup \{\neg A\}</math> sia inconsistente. Allora da esso è possibile derivare qualsiasi formula, dunque abbiamo che <math>\Gamma, \neg A \vdash A</math>. Per il teorema di deduzione, si ha che <math>\Gamma \vdash \neg A \to A</math>. Essendo <math>
▲:<math>\Gamma \vDash A</math> implica <math>\Gamma \vdash A</math>.
(\neg A \to A) \to A
</math> un [[Logica/Calcolo delle proposizioni/Sistema di Hilbert#Consequentia mirabilis|teorema]], per MP otteniamo <math>\Gamma \vdash A</math>.
Se <math>\Gamma</math> è un insieme di formule consistente, allora, per ogni formula <math>A</math>, <math>\Gamma \cup \{A\}</math> oppure <math>\Gamma \cup \{\neg A\}</math> è consistente.
''Dimostrazione''
Supponiamo, per assurdo, che <math>\Gamma</math>sia consistente, ma sia <math>\Gamma \cup \{A\}</math>che <math>\Gamma \cup \{\neg A\}</math>siano inconsistenti. Siccome <math>\Gamma \cup \{A\}</math> è inconsistente, per il lemma 1 abbiamo che <math>\Gamma \vdash \neg A</math>. Ma, essendo pure <math>\Gamma \cup \{\neg A\}</math> inconsistente, abbiamo anche <math>\Gamma \vdash A</math>. Dunque, <math>\Gamma</math> è inconsistente. Contraddizione.
==== Dimostrazione ====
Se <math>\Gamma</math>è inconsistente, la tesi è dimostrata. Supponiamo dunque che <math>\Gamma</math> sia un insieme di formule consistente.
Sia <math>A_0,A_1,A_2...</math> l'enumerazione di tutte le formule del linguaggio <math>\mathcal{L}</math>. Definiamo, per induzione, una sequenza di insiemi di formule:<blockquote><math>\Delta_0=\Gamma;</math></blockquote><blockquote><math>\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}</math></blockquote>Per ogni <math>i \in \N</math>, l'esistenza di <math>\Delta_i</math> è giustificata dal lemma 2 e, per costruzione, ogni <math>\Delta_i</math>è consistente.
Sia <math>\Delta = \bigcup_i \Delta_i</math>.
== Regole derivate ==
| |||