Wikibooks

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

Naviga nella cronologia in modo interattivo
← Differenza precedenteDifferenza successiva →
Contenuto cancellato Contenuto aggiunto
VisualeWikitesto
Nessun oggetto della modifica
Riga 122:
(<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/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>.
Riga 152:
Per il teorema di deduzione, abbiamo che <math> \vdash \neg A \to (A \to B) </math>. Dunque, <math> \neg A, A \vdash B </math> sse <math> \vdash \neg A \to (A \to B) </math>.
 
Essendo <math> \neg A \to (A \to B) </math> un [[Logica/Calcolo delle proposizioni/Sistema di Hilbert#EsempiTeorema didello dimostrazioniPseudo-Scoto|teorema]], effettivamente vale <math> \neg A, A \vdash B </math>, e, per taglio sulle premesse, si ha che <math>\Gamma \vdash B</math> per ogni formula <math> B</math>.
 
Dunque, per contrapposizione, se esiste una formula <math> B</math> tale che <math>\Gamma \nvdash B</math>, allora non esiste una proposizione <math>A</math> tale che <math>\Gamma \vdash A</math> e <math>\Gamma \vdash \neg A</math>.
Riga 238:
==== Enunciato ====
 
:<math>\Gamma \vDash A \to B</math> implica <math>\Gamma \vdash A \to B</math>.
 
== Regole derivate ==
Riga 256:
</math>
 
DerivaSi direttamentederiva dallo schema ''c'' con il teorema di deduzione.
 
====== Regola di transitività ======
Riga 262:
A \to B,\quad B \to C \over A \to C
</math>
 
Corrisponde al [[Logica/Calcolo delle proposizioni/Sistema di Hilbert#Sillogismo ipotetico|sillogismo ipotetico]].
 
====== Regola di scambio delle premesse ======
Line 275 ⟶ 277:
''Dimostrazione''
 
EssendoDa <math> \vdash \neg A \to (A \to B) </math> un (teorema dello Pseudo-Scoto), per il teorema di deduzione, si ha che <math> \neg A, A \vdash B </math>.
 
====== Consequentia mirabilis ======
Line 291 ⟶ 293:
# <math> \vdash (\neg A \to A) \to (\neg A \to \neg (\neg A \to A)) </math>: MP tra 2 e 3;
# <math> \neg A \to \neg (\neg A \to A) </math>: MP tra 1 e 4;
# <math> \vdash (\neg A \to \neg (\neg A \to A)) \to ((\neg A \to A) \to A) </math>: SUcontrapposizione indi ''c''5;
# <math> (\neg A \to A) \to A </math>: MP tra 51 e 6;.
# <math> A </math>: MP tra 1 e 7.▼
 
Quindi, <math>
Line 320 ⟶ 321:
Dunque, <math>
\neg\neg A \vdash A
</math>:, quindi, per il teorema di deduzione, su 1;<math>▼
\vdash \neg\neg A \to A▼
</math>.
 
Line 330 ⟶ 333:
 
# <math>
\vdash \neg\neg A \vdashto A
</math>: eliminazione della doppia negazione;
# <math>▼
▲\vdash \neg\neg A \to A
▲</math>: teorema di deduzione su 1;
# <math>
\vdash \neg\neg\neg A \to \neg A
</math>: SU in 21 con <math>
\neg A
</math> al posto di <math> A </math>;
# <math>▼
\vdash (\neg\neg\neg A \to \neg A) \to (A \to \neg\neg A)▼
</math>: SU in ''c'';
# <math>
\vdash A \to \neg\neg A
</math>: MPcontrapposizione tradi 3 e 42;
# <math>
A \vdash \neg\neg A
</math>: teorema di deduzione su 53;
 
==== Modus Tollens ====
Line 355 ⟶ 352:
\neg B,\quad A \to B \over \neg A
</math>
 
''Dimostrazione''
 
# <math> A \to B </math>: MP tra 3 e 4.ipotesi;▼
# <math>\neg B</math>: ipotesi;
▲# <math>
\vdash \neg\neg A \to A
</math>: eliminazione della doppia negazione;
▲# <math>
\neg\neg A \to B
</math>: sillogismo ipotetico tra 3 e 1;
# <math>
\vdash B \to \neg\neg B
</math>: introduzione della doppia negazione;
# <math>
▲\vdash (\neg\neg\neg A \to \neg A) \to (A \to \neg\neg A)B
</math>: sillogismo ipotetico tra 4 e 5;
# <math>
\neg B \to \neg A
</math>: contrapposizione di 6;
▲# <math>\neg A </math>: MP tra 12 e 7.
 
Dunque, <math>
\neg B, A \to B \vdash \neg A
</math>.
 
Applicando il teorema di deduzione, abbiamo la contrapposizione all'inverso: <math>
A \to B \vdash \neg B \to \neg A
</math>.
 
== Esempi di dimostrazioni ==
Line 394 ⟶ 420:
# <math> \vdash \neg A \to (\neg B \to \neg A) </math>: SU in ''a'';
# <math> \neg B \to \neg A </math>: MP tra 1 e 2;
# <math> \vdash (\neg B \to \neg A) \to (A \to B) </math>: SUcontrapposizione indi ''c'';3.
▲# <math> A \to B </math>: MP tra 3 e 4.
 
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>.
Estratto da "https://it.wikibooks.org/wiki/Logica_matematica/Calcolo_delle_proposizioni/Sistema_di_Hilbert"