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

Contenuto cancellato Contenuto aggiunto
Riga 257:
# Ciascun <math>\Delta_i</math> è consistente (per induzione: <math>\Delta_0=\Gamma</math> è consistente; il passo induttivo è giustificato dal lemma 2).
# <math>\Delta</math> è consistente. Supponiamo per assurdo che non lo sia. Allora esiste una formula <math>F</math>tale che <math>\Delta \vdash F</math> e <math>\Delta \vdash \neg F</math>. Quindi, per compattezza, esistono due insiemi finiti <math>\Delta_i, \Delta_j \subseteq \Delta</math> tali che <math>\Delta_i \vdash F</math> e <math>\Delta_j \vdash \neg F</math>. Per costruzione, abbiamo che <math>\Delta_i \subseteq \Delta_j</math> oppure <math>\Delta_j \subseteq \Delta_i</math>. Se <math>\Delta_i \subseteq \Delta_j</math>, per monotonia si ha che <math>\Delta_j \vdash F</math>, dunque <math>\Delta_j</math> è inconsistente, contraddizione con il punto 3. Viceversa, se <math>\Delta_j \subseteq \Delta_i</math>, per monotonia si ha che <math>\Delta_i \vdash \neg F</math>, dunque <math>\Delta_i</math> è inconsistente, contraddizione con il punto 3.
# Per ogni formula <math>F</math>, <math>\neg F \in \Delta</math> sse <math>F \not\in \Delta</math>. Supponiamo che <math>F \not\in \Delta</math>. Allora, essendo <math>\Delta</math> massimale, abbiamo che <math>\neg F \in \Delta</math>. Supponiamo per assurdo che <math>\neg F \in \Delta</math>, ma <math>F \in \Delta</math>. Allora, per inclusione, si ha che <math>\Delta \vdash \neg F</math> e <math>\Delta \vdash F</math>, dunque, <math>\Delta</math> è inconsistente. Contraddizione con il punto 4.
# Per ogni formula <math>F</math>, se <math>\Delta \vdash F</math> allora <math>F \in \Delta</math>. Supponiamo per assurdo che <math>\Delta \vdash F</math>, ma <math>F \not\in \Delta</math>. Allora, per il punto 5, abbiamo che <math>\neg F \in \Delta</math>, quindi, per inclusione, <math>\Delta \vdash \neg F</math>, dunque, <math>\Delta</math> è inconsistente. Contraddizione con il punto 4.
 
== Regole derivate ==