¿Cómo puedo demostrar $x \vee \neg x$ en el sistema Hilbert?

Question

Cómo demostrar $x \vee \neg x$ utilizando los siguientes axiomas?

1. $A \rightarrow (B \rightarrow A)$
2. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
3. $(A \wedge B) \rightarrow A$
4. $(A \wedge B) \rightarrow B$
5. $(A \rightarrow B) \rightarrow ((A \rightarrow C) \rightarrow (A \rightarrow B \wedge C))$
6. $A \rightarrow A \vee B$
7. $B \rightarrow A \vee B$
8. $(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow (A \vee B \rightarrow C))$
9. $A \rightarrow \neg \neg A$
10. $\neg \neg A \rightarrow A$
11. $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$

Lo que estoy pensando es que usando 6 o 7, primero tendría que probar $x$ que no es una tautología y usando 8, podría demostrar $x \vee \neg x \rightarrow C$ pero no importa lo que ponga en lugar de $C$ no podré invertir la flecha. ¿Puede alguna afirmación ser imposible de demostrar? ¿Es un mal conjunto de axiomas el que estoy utilizando?

Answer 1

1. Prueba $\lnot (x \land \lnot x)$ . Esto es fácil en deducción natural, pero en un sistema de Hilbert se requiere algo más de esfuerzo. (O, hacer trampa y utilizar el teorema de la deducción.) Usted no tendrá que utilizar la eliminación doble negación aquí.

2. Demostrar la ley de Morgan en la forma $\lnot (p \land q)$ implica $\lnot p \lor \lnot q$ .

3. Junte los dos pasos anteriores para obtener $\lnot x \lor \lnot \lnot x$ y, a continuación, aplicar la eliminación de la doble negación.

Answer 2

Me gustaría dar una nueva prueba, espero que un poco "más legible".

Me refiero a Elliott Mendelson, Introducción a la lógica matemática (4ª ed. - 1997).

El 11-axioms OP's sistema axiomático es como el sistema de 10 ejes $\mathsf L_4$ discutido en Mendelson [página 46], derivado de Kleene [1952 - Introducción a las metamatemáticas ] con una "variante" en Ax5, y Ax9 y Ax11 en lugar del axioma 10 de Kleene : $\vdash (B \rightarrow C) \rightarrow ((B \rightarrow \lnot C) \rightarrow \lnot C)$ .

Ax1 y Ax2 también se utilizan en Mendelson [como (A1) y (A2) ].

Lema 0 : $\vdash A \rightarrow A$ [ Self-Imp - véase Mendelson : Lema 1.8 página 36]

(1) $\vdash [A \rightarrow ((B \rightarrow A) \rightarrow A)] \rightarrow [(A \rightarrow (B \rightarrow A)) \rightarrow (A \rightarrow A)]$ --- Ax2

(2) $\vdash A \rightarrow ((B \rightarrow A) \rightarrow A)$ --- Ax1

(3) $\vdash (A \rightarrow (B \rightarrow A)) \rightarrow (A \rightarrow A)$ --- a partir de (1) y (2) mediante modus ponens

(4) $\vdash A \rightarrow (B \rightarrow A)$ --- Ax1

(5) $\vdash A \rightarrow A$ --- a partir de (3) y (4) mediante modus ponens .

Con Ax1, Ax2 y Lema 0 podemos demostrar que Teorema de la deducción [véase Mendelson : Proposición 1.9 página 37].

Lema 1 : $A \rightarrow B, B \rightarrow C \vdash A \rightarrow C$ [ Silogismo - véase Mendelson : Corolario 1.10a página 38]

(1) $A \rightarrow B$ --- asumido

(2) $B \rightarrow C$ --- asumido

(3) $\vdash (B \rightarrow C) \rightarrow (A \rightarrow (B \rightarrow C))$ --- Ax1

(4) $A \rightarrow (B \rightarrow C)$ --- a partir de (2) y (3) mediante modus ponens

(5) $\vdash [A \rightarrow (B \rightarrow C)] \rightarrow [(A \rightarrow B) \rightarrow (A \rightarrow C)]$ --- Ax2

(6) $(A \rightarrow B) \rightarrow (A \rightarrow C)$ --- a partir de (4) y (5) mediante modus ponens

(7) $A \rightarrow C$ --- a partir de (1) y (6) mediante modus ponens .

Lema 2 : $\vdash (\lnot A \rightarrow \lnot B) \rightarrow (B \rightarrow A)$ [ Transposición ]

(1) $\vdash (\lnot A \rightarrow \lnot B) \rightarrow (\lnot \lnot B \rightarrow \lnot \lnot A)$ --- Ax11

(2) $\lnot A \rightarrow \lnot B$ --- asumido

(3) $\lnot \lnot B \rightarrow \lnot \lnot A$ --- a partir de (1) y (2) mediante modus ponens

(4) $\vdash B \rightarrow \lnot \lnot B$ --- Ax9

(5) $B \rightarrow \lnot \lnot A$ --- a partir de (3) y (4) mediante Syll

(6) $\vdash \lnot \lnot A \rightarrow A$ --- Ax10

(7) $B \rightarrow A$ --- a partir de (5) y (6) mediante Syll

(8) $\vdash (\lnot A \rightarrow \lnot B) \rightarrow (B \rightarrow A)$ --- por Teorema de la deducción descargando (2).

Lema 3 : $\vdash \lnot A \rightarrow (A \rightarrow B)$

(1) $\vdash \lnot A \rightarrow (\lnot B \rightarrow \lnot A)$ --- Ax1

(2) $\vdash (\lnot B \rightarrow \lnot A) \rightarrow (A \rightarrow B)$ --- Lema 2

(3) $\vdash \lnot A \rightarrow (A \rightarrow B)$ --- a partir de (1) y (2) mediante Syll .

Lema 4 : $\vdash (\lnot A \rightarrow A) \rightarrow (B \rightarrow A)$

(1) $\vdash \lnot A \rightarrow (A \rightarrow \lnot B)$ --- Lema 3

(2) $\vdash [\lnot A \rightarrow (A \rightarrow \lnot B)] \rightarrow [(\lnot A \rightarrow A) \rightarrow (\lnot A \rightarrow \lnot B)]$ --- Ax2

(3) $\vdash (\lnot A \rightarrow A) \rightarrow (\lnot A \rightarrow \lnot B)$ --- a partir de (1) y (2) mediante modus ponens

(4) $\vdash (\lnot A \rightarrow \lnot B) \rightarrow (B \rightarrow A)$ --- Lema 2

(5) $\vdash (\lnot A \rightarrow A) \rightarrow (B \rightarrow A)$ --- a partir de (3) y (4) mediante Syll .

Lema 5 : $\vdash (\lnot A \rightarrow A) \rightarrow A$

(1) $\vdash (\lnot A \rightarrow A) \rightarrow ((\lnot A \rightarrow A) \rightarrow A)$ --- Lema 4

(2) $\vdash [(\lnot A \rightarrow A) \rightarrow ((\lnot A \rightarrow A) \rightarrow A)] \rightarrow [ ((\lnot A \rightarrow A) \rightarrow (\lnot A \rightarrow A)) \rightarrow ((\lnot A \rightarrow A) \rightarrow A) ]$ --- Ax2

(3) $\vdash ((\lnot A \rightarrow A) \rightarrow (\lnot A \rightarrow A)) \rightarrow ((\lnot A \rightarrow A) \rightarrow A)$ --- a partir de (1) y (2) mediante modus ponens

(4) $\vdash (\lnot A \rightarrow A) \rightarrow (\lnot A \rightarrow A)$ --- Lema 0

(5) $\vdash (\lnot A \rightarrow A) \rightarrow A$ --- a partir de (3) y (4) mediante modus ponens .

Lema 6 : $A \rightarrow B, \lnot A \rightarrow B \vdash B$

(1) $A \rightarrow B$ --- asumido

(2) $\vdash (A \rightarrow B) \rightarrow (\lnot B \rightarrow \lnot A)$ --- Ax11

(3) $\lnot B \rightarrow \lnot A$ --- a partir de (1) y (2) mediante modus ponens

(4) $\lnot A \rightarrow B$ --- asumido

(5) $\lnot B \rightarrow B$ --- a partir de (3) y (4) mediante Syll

(6) $\vdash (\lnot B \rightarrow B) \rightarrow B$ --- Lema 5

(7) $B$ --- a partir de (5) y (6) mediante modus ponens .

Por último, tenemos nuestro resultado principal :

Teorema [Medio Excluido] : $\vdash A \lor \lnot A$

(1) $\vdash A \rightarrow (A \lor \lnot A)$ --- Ax6

(2) $\vdash \lnot A \rightarrow (A \lor \lnot A)$ --- Ax7

(3) $\vdash A \lor \lnot A$ --- a partir de (1) y (2) mediante Lema 6 .

---

Notas

(A) Hemos utilizado el Teorema de la deducción sólo en la prueba de Lema 2 con un poco de esfuerzo adicional podemos evitarlo por completo.

(B) Sólo hemos utilizado Ax1, Ax2, Ax6, Ax7, Ax9, Ax10, Ax11.

Answer 3

Lema 1: $(P \rightarrow Q) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q))$

1. $(R \rightarrow (P \rightarrow Q)) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q))$ Axioma 2
2. $((R \rightarrow (P \rightarrow Q))\rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q))) \rightarrow ((P \rightarrow Q) \rightarrow ((R \rightarrow (P \rightarrow Q)) \rightarrow ((R \rightarrow P) \rightarrow (R\rightarrow Q))))$ Axioma 1
3. $(P \rightarrow Q) \rightarrow ((R \rightarrow (P \rightarrow Q)) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q)))$ 1,2 MP
4. $((P \rightarrow Q) \rightarrow ((R \rightarrow (P \rightarrow Q)) \rightarrow ((R \rightarrow P) \rightarrow (R\rightarrow Q))))\rightarrow (((P \rightarrow Q) \rightarrow (R \rightarrow (P \rightarrow Q))) \rightarrow ((P \rightarrow Q) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q))))$ Axioma 2
5. $((P \rightarrow Q) \rightarrow (R \rightarrow (P \rightarrow Q))) \rightarrow ((P \rightarrow Q) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q)))$ 3,4 MP
6. $(P \rightarrow Q) \rightarrow (R \rightarrow (P \rightarrow Q))$ Axioma 1
7. $(P \rightarrow Q) \rightarrow ((R\rightarrow P) \rightarrow (R \rightarrow Q))$ 5,6 MP

Lema 2: $(P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q)$

1. $((P \rightarrow (P \rightarrow Q)) \rightarrow ((P \rightarrow P) \rightarrow (P \rightarrow Q))) \rightarrow (((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P)) \rightarrow ((P\rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q)))$ Axioma 2
2. $(P \rightarrow (P \rightarrow Q)) \rightarrow ((P \rightarrow P) \rightarrow (P \rightarrow Q))$ Axioma 2
3. $((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P)) \rightarrow ((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q))$ 1,2 MP
4. $P \rightarrow ((P \rightarrow P) \rightarrow P)$ Axioma 1
5. $(P \rightarrow ((P \rightarrow P) \rightarrow P)) \rightarrow ((P \rightarrow (P \rightarrow P)) \rightarrow(P \rightarrow P))$ Axioma 2
6. $(P \rightarrow (P \rightarrow P)) \rightarrow (P \rightarrow P)$ 4,5 MP
7. $P \rightarrow (P \rightarrow P)$ Axioma 1
8. $P \rightarrow P$ 6,7 MP
9. $(P \rightarrow P) \rightarrow ((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P))$ Axioma 1
10. $(P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P)$ 8,9 MP
11. $(P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q)$ 3,10 MP

Lema 3: $P \rightarrow ((P \rightarrow Q) \rightarrow Q)$

1. $(P \rightarrow Q) \rightarrow (((P \rightarrow Q) \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q))$ Axioma 1
2. $((P \rightarrow Q) \rightarrow (((P\rightarrow Q) \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q))) \rightarrow (((P \rightarrow Q) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow Q))) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow Q)))$ Axioma 2
3. $((P \rightarrow Q) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow Q))) \rightarrow ((P\rightarrow Q)\rightarrow (P \rightarrow Q))$ 1,2 MP
4. $(P\rightarrow Q) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow Q))$ Axioma 1
5. $(P \rightarrow Q) \rightarrow (P \rightarrow Q)$ 3,4 MP
6. $((P \rightarrow Q) \rightarrow (P \rightarrow Q)) \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P\rightarrow Q) \rightarrow Q))$ Axioma 2
7. $((P\rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)$ 5,6 MP
8. $P \rightarrow ((P\rightarrow Q) \rightarrow P)$ Axioma 1
9. $((P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) > Q))) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))) \rightarrow ((((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q))) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))))$ Axioma 1
10. $(P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q))) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))$ Axioma 2
11. $(((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q))) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q))))$ 9,10 MP
12. $((((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P\rightarrow Q) \rightarrow Q))) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q))))) \rightarrow (((((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow (P \rightarrow (((P\rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)))) \rightarrow ((((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))))$ Axioma 2
13. $((((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow (P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)))) \rightarrow ((((P \rightarrow Q) \rightarrow P) > ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q))))$ 11,12 MP
14. $(((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow (P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)))$ Axioma 1
15. $(((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))$ 13,14 MP
16. $(P\rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q))$ 7,15 MP
17. $P \rightarrow ((P \rightarrow Q) \rightarrow Q)$ 8,16 MP

Teorema principal: $P \vee \neg P$

1. $P \rightarrow (P \vee \neg P)$ Axioma 6
2. $(P \rightarrow (P \vee \neg P)) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg P)$ Axioma 11
3. $\neg (P \vee \neg P) \rightarrow \neg P$ 1,2 MP
4. $\neg P \rightarrow (P \vee \neg P)$ Axioma 7
5. $(\neg P \rightarrow (P \vee \neg P)) \rightarrow ((\neg (P \vee \neg P) \rightarrow \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))$ Lema 1
6. $(\neg (P \vee \neg P) \rightarrow \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))$ 4,5 MP
7. $\neg (P \vee \neg P) \rightarrow (P \vee \neg P)$ 3,6 MP
8. $\neg (P \vee \neg P) \rightarrow ((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P))$ Lema 3
9. $((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P)) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))$ Axioma 11
10. $(((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P)) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))) \rightarrow ((\neg (P \vee \neg P) \rightarrow ((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P))) \rightarrow (\neg (P \vee \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))))$ Lema 1
11. $(~(P \vee \neg P) \rightarrow ((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P))) \rightarrow (\neg (P \vee \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))))$ 9,10 MP
12. $\neg (P \vee \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))$ 8,11 MP
13. $(\neg (P \vee \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))$ Lema 2
14. $~(P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))$ 12,13 PM
15. $(\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))) \rightarrow (\neg\neg(\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow \neg \neg(P \vee \neg P)) $ Axioma 11
16. $\neg\neg(\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow \neg\neg(P \vee \neg P)$ 14,15 PM
17. $(\neg (P \vee\neg P) \rightarrow (P \vee \neg P)) \rightarrow \neg\neg (\neg(P \vee \neg P) \rightarrow (P \vee \neg P))$ Axioma 9
18. $\neg \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))$ 7,17 MP
19. $\neg\neg (P \vee \neg P)$ 16,18 MP
20. $\neg\neg (P \vee \neg P) \rightarrow (P \vee \neg P)$ Axioma 10
21. $P \vee \neg P$ 19,20 MP