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

Contenuto cancellato Contenuto aggiunto
Riga 217:
:<math>\Gamma \vDash A</math> implica <math>\Gamma \vdash A</math>.
 
Per dimostrare il teorema di completezza, ci serviremoserviamo dei seguenti lemmi.
 
==== Lemma 1 ====
Riga 238:
 
==== Lemma 3 ====
Sia <math>\Gamma</math>un insieme di formule. Se <math>\Gamma</math> è insoddisfacibile, allora <math>\Gamma</math>è inconsistente.
 
''Dimostrazione''
Riga 259:
# 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.
# Per ogni formula <math>A</math> e <math>B</math>, <math>A \to B \in \Delta</math> sse <math>A \not\in \Delta</math> o <math>B \in \Delta</math>. Supponiamo per assurdo che <math>A \to B \in \Delta</math>, <math>A \in \Delta</math> e <math>B \not\in \Delta</math>. Per inclusione, abbiamo che <math>\Delta \vdash A \to B</math> e <math>\Delta \vdash A</math>, pertanto, per MP, <math>\Delta \vdash B</math> e, per il punto 6, <math>B \in \Delta</math>; contraddizione. Se <math>A \not\in \Delta</math>, allora, per il punto 5, <math>\neg A \in \Delta</math>. Per inclusione, abbiamo che <math>\Delta \vdash \neg A</math>. Essendo <math> \neg A \to (A \to B) </math> un [[Logica/Calcolo delle proposizioni/Sistema di Hilbert#Teorema dello Pseudo-Scoto|teorema]], per MP otteniamo <math>\Delta \vdash A \to B</math>, dunque <math>A \to B \in \Delta</math>. Se <math>B \in \Delta</math>, allora, per inclusione, abbiamo <math>\Delta \vdash B</math>. Per monotonia, si ha che <math>\Delta, A \vdash B</math>, quindi, per il teorema di deduzione, otteniamo <math>\Delta \vdash A \to B</math>, dunque <math>A \to B \in \Delta</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:<blockquote><math>\mathcal{M_V}=\{p|p \in \mathcal{P}, p \in \Delta\}</math></blockquote>dove <math>\mathcal{P}</math> è l'insieme dei simboli proposizionali del linguaggio.
Riga 265:
Dimostriamo ora, per induzione strutturale sulle formule, che per ogni formula <math>F</math>:<blockquote><math>F \in \Delta</math> sse <math>\mathcal{M_V} \models F</math>.</blockquote>(''Passo base'') Per costruzione di <math>\mathcal{M_V}</math>.
 
(''Passo induttivo'') Sia <math>F=\neg A</math>. Abbiamo che <math>\mathcal{M_V} \models \neg A</math> sse <math>\mathcal{M_V} \nvDash A</math>sse <math>A \not\in \Delta</math>sse <math>\neg A \in \Delta</math>.
(''Passo induttivo'')
 
Sia <math>F=A \to B</math>. Abbiamo che <math>\mathcal{M_V} \models A \to B</math> sse <math>\mathcal{M_V} \nvDash A</math>o <math>\mathcal{M_V} \models B</math> sse <math>A \not\in \Delta</math> o <math>B \in \Delta</math> sse <math>A \to B \in \Delta</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.
 
==== Dimostrazione ====
Supponiamo che <math>\Gamma \vDash A</math>. Allora, per il teorema di soddisfacibilità, <math>\Gamma \cup \{\neg A\}</math> è insoddisfacibile e, per il lemma 3, è anche inconsistente. Dunque, per il lemma 1, <math>\Gamma \vdash A</math>.
 
== Regole derivate ==
 
Line 474 ⟶ 482:
Abbiamo dimostrato che <math> \neg A \vdash A \to B </math>. Dunque, per il teorema di deduzione, <math> \vdash \neg A \to (A \to B) </math>.
 
{{avanzamento|75100%}}
 
[[Categoria:Logica|Sistema di Hilbert]]