Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
Riga 263:
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.
Dimostriamo ora, per induzione strutturale sulle formule, che per ogni formula <math>F</math>:<blockquote><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> (per definizione) sse <math>A \not\in \Delta</math> (per ipotesi induttiva) sse <math>\neg A \in \Delta</math> (per il punto 5).
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> (per definizione) sse <math>A \not\in \Delta</math> o <math>B \in \Delta</math> (per ipotesi induttiva) sse <math>A \to B \in \Delta</math> (per il punto 7).
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.
| |||