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

Contenuto cancellato Contenuto aggiunto
Riga 261:
# 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 matematica/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 274:
 
==== Dimostrazione ====
Supponiamo che <math>\Gamma \vDash A</math>. Allora, per il [[Logica matematica/Calcolo delle proposizioni#Teorema di soddisfacibilità|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 ==
Riga 299:
</math>
 
Corrisponde al [[Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert#Sillogismo ipotetico|sillogismo ipotetico]].
 
====== Regola di scambio delle premesse ======