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

Contenuto cancellato Contenuto aggiunto
Riga 230:
(<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>
(\neg A \to A) \to A
</math> un [[Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert#Consequentia mirabilis|teorema]], per MP otteniamo <math>\Gamma \vdash A</math>.
 
==== Lemma 2 ====