Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
correggo template e categoria |
|||
Riga 124:
(<math>\Rightarrow</math>) Sia <math>A_1,...,A_n=A</math> una dimostrazione di <math>A</math> da <math>\Gamma \cup \{B\}</math>. Procediamo per induzione completa.
(''Passo base'') <math>A_1 \in \Gamma</math>, oppure <math>A_1</math> è un assioma, oppure è <math>B</math> stesso. Per lo schema ''a'' abbiamo <math>A_1 \to (B \to A_1)</math>, dunque, se <math>A_1 \in \Gamma</math> o <math>A_1</math> è un assioma, abbiamo per MP che <math>\Gamma \vdash B \to A_1</math>. Se <math>A_1=B</math>, siccome <math> B \to B </math> è un [[Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert#Riflessività dell'implicazione|teorema]], abbiamo <math>\Gamma \vdash B \to B</math>.
(''Passo induttivo'') Supponiamo che <math>\Gamma \vdash B \to A_i</math>, per ogni <math>i<n</math>. Consideriamo <math>A_n</math>. Come sopra, se <math>A_n \in \Gamma</math> o <math>A_n</math> è un assioma o <math>A_n=B</math> abbiamo che <math>\Gamma \vdash B \to A_n</math>. Supponiamo allora che <math>A_n</math> sia stato derivato per MP. Dunque, lo si è ottenuto da due formule <math>A_j</math>, <math>A_k=A_j \to A_n</math>, <math>j,k<n</math>. Per ipotesi induttiva, <math>\Gamma \vdash B \to A_j</math> e <math>\Gamma \vdash B \to A_k</math>. <math>A_k</math> è della forma <math>A_j \to A_n</math>, dunque abbiamo <math>\Gamma \vdash B \to (A_j \to A_n)</math>. Per lo schema di assioma ''b,'' abbiamo che <math>(B \to (A_j \to A_n)) \to ((B \to A_j) \to (B \to A_n))</math>. Da questa formula, da <math>B \to (A_j \to A_n)</math> e da <math>B \to A_j</math>, applicando due volte MP, si ha <math>\Gamma \vdash B \to A_n</math>.
| |||