for questions or link request: module admin

First theorems of Propositional Calculus

name: prophilbert1, module version: 1.00.00, rule version: 1.00.00, original: prophilbert1, author of this module: Michael Meyling

Description

This module includes first proofs of propositional calculus theorems. The following theorems and proofs are adapted from D. Hilbert and W. Ackermann's `Grundzuege der theoretischen Logik' (Berlin 1928, Springer)

References

This document uses the results of the following documents:

Content

First we prove a simple implication, that follows directly from the fourth axiom:

1. Proposition
      (P → Q) → ((A → P) → (A → Q))     (hilb1)

Proof:
1 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
2 (P → Q) → ((¬A ∨ P) → (¬A ∨ Q)) replace proposition variable A by ¬A in 1
3 (P → Q) → ((A → P) → (¬A ∨ Q)) reverse abbreviation impl in 2 at occurence 1
4 (P → Q) → ((A → P) → (A → Q)) reverse abbreviation impl in 3 at occurence 1
qed

This proposition is the form for the Hypothetical Syllogism.


The self implication could be derived:

2. Proposition
      P → P     (hilb2)

Proof:
1 P → (P ∨ Q) add axiom axiom2
2 P → (P ∨ P) replace proposition variable Q by P in 1
3 (P ∨ P) → P add axiom axiom1
4 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
5 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 4
6 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 5
7 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 6
8 (D → C) → ((P → D) → (P → C)) replace proposition variable B by P in 7
9 (D → P) → ((P → D) → (P → P)) replace proposition variable C by P in 8
10 ((P ∨ P) → P) → ((P → (P ∨ P)) → (P → P)) replace proposition variable D by P ∨ P in 9
11 (P → (P ∨ P)) → (P → P) modus ponens with 3, 10
12 P → P modus ponens with 2, 11
qed

One form of the classical `tertium non datur'

3. Proposition
      ¬P ∨ P     (hilb3)

Proof:
1 P → P add proposition hilb2
2 ¬P ∨ P use abbreviation impl in 1 at occurence 1
qed

The standard form of the excluded middle:

4. Proposition
      P ∨ ¬P     (hilb4)

Proof:
1 ¬P ∨ P add proposition hilb3
2 (P ∨ Q) → (Q ∨ P) add axiom axiom3
3 (P ∨ A) → (A ∨ P) replace proposition variable Q by A in 2
4 (B ∨ A) → (A ∨ B) replace proposition variable P by B in 3
5 (B ∨ P) → (P ∨ B) replace proposition variable A by P in 4
6 (¬P ∨ P) → (P ∨ ¬P) replace proposition variable B by ¬P in 5
7 P ∨ ¬P modus ponens with 1, 6
qed

Double negation is implicated:

5. Proposition
      P → ¬¬P     (hilb5)

Proof:
1 P ∨ ¬P add proposition hilb4
2 ¬P ∨ ¬¬P replace proposition variable P by ¬P in 1
3 P → ¬¬P reverse abbreviation impl in 2 at occurence 1
qed

The reverse is also true:

6. Proposition
      ¬¬P → P     (hilb6)

Proof:
1 P → ¬¬P add proposition hilb5
2 ¬P → ¬¬¬P replace proposition variable P by ¬P in 1
3 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
4 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 3
5 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 4
6 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 5
7 (D → C) → ((P ∨ D) → (P ∨ C)) replace proposition variable B by P in 6
8 (D → ¬¬¬P) → ((P ∨ D) → (P ∨ ¬¬¬P)) replace proposition variable C by ¬¬¬P in 7
9 (¬P → ¬¬¬P) → ((P ∨ ¬P) → (P ∨ ¬¬¬P)) replace proposition variable D by ¬P in 8
10 (P ∨ ¬P) → (P ∨ ¬¬¬P) modus ponens with 2, 9
11 P ∨ ¬P add proposition hilb4
12 P ∨ ¬¬¬P modus ponens with 11, 10
13 (P ∨ Q) → (Q ∨ P) add axiom axiom3
14 (P ∨ A) → (A ∨ P) replace proposition variable Q by A in 13
15 (B ∨ A) → (A ∨ B) replace proposition variable P by B in 14
16 (B ∨ ¬¬¬P) → (¬¬¬P ∨ B) replace proposition variable A by ¬¬¬P in 15
17 (P ∨ ¬¬¬P) → (¬¬¬P ∨ P) replace proposition variable B by P in 16
18 ¬¬¬P ∨ P modus ponens with 12, 17
19 ¬¬P → P reverse abbreviation impl in 18 at occurence 1
qed

The correct reverse of an implication:

7. Proposition
      (P → Q) → (¬Q → ¬P)     (hilb7)

Proof:
1 P → ¬¬P add proposition hilb5
2 Q → ¬¬Q replace proposition variable P by Q in 1
3 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
4 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 3
5 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 4
6 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 5
7 (D → C) → ((¬P ∨ D) → (¬P ∨ C)) replace proposition variable B by ¬P in 6
8 (D → ¬¬Q) → ((¬P ∨ D) → (¬P ∨ ¬¬Q)) replace proposition variable C by ¬¬Q in 7
9 (Q → ¬¬Q) → ((¬P ∨ Q) → (¬P ∨ ¬¬Q)) replace proposition variable D by Q in 8
10 (¬P ∨ Q) → (¬P ∨ ¬¬Q) modus ponens with 2, 9
11 (P ∨ Q) → (Q ∨ P) add axiom axiom3
12 (P ∨ A) → (A ∨ P) replace proposition variable Q by A in 11
13 (B ∨ A) → (A ∨ B) replace proposition variable P by B in 12
14 (B ∨ ¬¬Q) → (¬¬Q ∨ B) replace proposition variable A by ¬¬Q in 13
15 (¬P ∨ ¬¬Q) → (¬¬Q ∨ ¬P) replace proposition variable B by ¬P in 14
16 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
17 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 16
18 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 17
19 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 18
20 (D → C) → (((¬P ∨ Q) → D) → ((¬P ∨ Q) → C)) replace proposition variable B by ¬P ∨ Q in 19
21 (D → (¬¬Q ∨ ¬P)) → (((¬P ∨ Q) → D) → ((¬P ∨ Q) → (¬¬Q ∨ ¬P))) replace proposition variable C by ¬¬Q ∨ ¬P in 20
22 ((¬P ∨ ¬¬Q) → (¬¬Q ∨ ¬P)) → (((¬P ∨ Q) → (¬P ∨ ¬¬Q)) → ((¬P ∨ Q) → (¬¬Q ∨ ¬P))) replace proposition variable D by ¬P ∨ ¬¬Q in 21
23 ((¬P ∨ Q) → (¬P ∨ ¬¬Q)) → ((¬P ∨ Q) → (¬¬Q ∨ ¬P)) modus ponens with 15, 22
24 (¬P ∨ Q) → (¬¬Q ∨ ¬P) modus ponens with 10, 23
25 (P → Q) → (¬¬Q ∨ ¬P) reverse abbreviation impl in 24 at occurence 1
26 (P → Q) → (¬Q → ¬P) reverse abbreviation impl in 25 at occurence 1
qed

Definition of an Implication 1. part:

8. Proposition
      (P → Q) → (¬P ∨ Q)     (defimpl1)

Proof:
1 P → P add proposition hilb2
2 A → A replace proposition variable P by A in 1
3 (P → Q) → (P → Q) replace proposition variable A by P → Q in 2
4 (P → Q) → (¬P ∨ Q) use abbreviation impl in 3 at occurence 3
qed

Definition of an Implication 2. part:

9. Proposition
      (¬P ∨ Q) → (P → Q)     (defimpl2)

Proof:
1 P → P add proposition hilb2
2 A → A replace proposition variable P by A in 1
3 (P → Q) → (P → Q) replace proposition variable A by P → Q in 2
4 (¬P ∨ Q) → (P → Q) use abbreviation impl in 3 at occurence 2
qed

Definition of a Conjunction 1. part:

10. Proposition
      (P ∧ Q) → ¬(¬P ∨ ¬Q)     (defand1)

Proof:
1 P → P add proposition hilb2
2 A → A replace proposition variable P by A in 1
3 (P ∧ Q) → (P ∧ Q) replace proposition variable A by P ∧ Q in 2
4 (P ∧ Q) → ¬(¬P ∨ ¬Q) use abbreviation and in 3 at occurence 2
qed

Definition of a Conjunction 2. part:

11. Proposition
      ¬(¬P ∨ ¬Q) → (P ∧ Q)     (defand2)

Proof:
1 P → P add proposition hilb2
2 A → A replace proposition variable P by A in 1
3 (P ∧ Q) → (P ∧ Q) replace proposition variable A by P ∧ Q in 2
4 ¬(¬P ∨ ¬Q) → (P ∧ Q) use abbreviation and in 3 at occurence 1
qed

Definition of an Equivalence 1. part:

12. Proposition
      (P ↔ Q) → ((P → Q) ∧ (Q → P))     (defequi1)

Proof:
1 P → P add proposition hilb2
2 A → A replace proposition variable P by A in 1
3 (P ↔ Q) → (P ↔ Q) replace proposition variable A by P ↔ Q in 2
4 (P ↔ Q) → ((P → Q) ∧ (Q → P)) use abbreviation equi in 3 at occurence 2
qed

Definition of an Equivalence 2. part:

13. Proposition
      ((P → Q) ∧ (Q → P)) → (P ↔ Q)     (defequi2)

Proof:
1 P → P add proposition hilb2
2 A → A replace proposition variable P by A in 1
3 (P ↔ Q) → (P ↔ Q) replace proposition variable A by P ↔ Q in 2
4 ((P → Q) ∧ (Q → P)) → (P ↔ Q) use abbreviation equi in 3 at occurence 1
qed

A simular formulation for the second axiom:

14. Proposition
      P → (Q ∨ P)     (hilb8)

Proof:
1 P → (P ∨ Q) add axiom axiom2
2 (P ∨ Q) → (Q ∨ P) add axiom axiom3
3 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
4 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 3
5 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 4
6 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 5
7 (D → C) → ((P → D) → (P → C)) replace proposition variable B by P in 6
8 (D → (Q ∨ P)) → ((P → D) → (P → (Q ∨ P))) replace proposition variable C by Q ∨ P in 7
9 ((P ∨ Q) → (Q ∨ P)) → ((P → (P ∨ Q)) → (P → (Q ∨ P))) replace proposition variable D by P ∨ Q in 8
10 (P → (P ∨ Q)) → (P → (Q ∨ P)) modus ponens with 2, 9
11 P → (Q ∨ P) modus ponens with 1, 10
qed

A technical lemma (equal to the third axiom):

15. Proposition
      (P ∨ Q) → (Q ∨ P)     (hilb9)

Proof:
1 (P ∨ Q) → (Q ∨ P) add axiom axiom3
qed

And another technical lemma (simular to the third axiom):

16. Proposition
      (Q ∨ P) → (P ∨ Q)     (hilb10)

Proof:
1 (P ∨ Q) → (Q ∨ P) add axiom axiom3
2 (P ∨ A) → (A ∨ P) replace proposition variable Q by A in 1
3 (B ∨ A) → (A ∨ B) replace proposition variable P by B in 2
4 (B ∨ P) → (P ∨ B) replace proposition variable A by P in 3
5 (Q ∨ P) → (P ∨ Q) replace proposition variable B by Q in 4
qed

A technical lemma (equal to the first axiom):

17. Proposition
      (P ∨ P) → P     (hilb11)

Proof:
1 (P ∨ P) → P add axiom axiom1
qed

A simple propositon that follows directly from the second axiom:

18. Proposition
      P → (P ∨ P)     (hilb12)

Proof:
1 P → (P ∨ Q) add axiom axiom2
2 P → (P ∨ P) replace proposition variable Q by P in 1
qed

This is a pre form for the associative law:

19. Proposition
      (P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A))     (hilb13)

Proof:
1 P → (Q ∨ P) add proposition hilb8
2 P → (B ∨ P) replace proposition variable Q by B in 1
3 C → (B ∨ C) replace proposition variable P by C in 2
4 C → (P ∨ C) replace proposition variable B by P in 3
5 A → (P ∨ A) replace proposition variable C by A in 4
6 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
7 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 6
8 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 7
9 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 8
10 (D → C) → ((Q ∨ D) → (Q ∨ C)) replace proposition variable B by Q in 9
11 (D → (P ∨ A)) → ((Q ∨ D) → (Q ∨ (P ∨ A))) replace proposition variable C by P ∨ A in 10
12 (A → (P ∨ A)) → ((Q ∨ A) → (Q ∨ (P ∨ A))) replace proposition variable D by A in 11
13 (Q ∨ A) → (Q ∨ (P ∨ A)) modus ponens with 5, 12
14 (D → C) → ((P ∨ D) → (P ∨ C)) replace proposition variable B by P in 9
15 (D → (Q ∨ (P ∨ A))) → ((P ∨ D) → (P ∨ (Q ∨ (P ∨ A)))) replace proposition variable C by Q ∨ (P ∨ A) in 14
16 ((Q ∨ A) → (Q ∨ (P ∨ A))) → ((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) replace proposition variable D by Q ∨ A in 15
17 (P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A))) modus ponens with 13, 16
18 (P ∨ Q) → (Q ∨ P) add proposition hilb9
19 (P ∨ B) → (B ∨ P) replace proposition variable Q by B in 18
20 (C ∨ B) → (B ∨ C) replace proposition variable P by C in 19
21 (C ∨ (Q ∨ (P ∨ A))) → ((Q ∨ (P ∨ A)) ∨ C) replace proposition variable B by Q ∨ (P ∨ A) in 20
22 (P ∨ (Q ∨ (P ∨ A))) → ((Q ∨ (P ∨ A)) ∨ P) replace proposition variable C by P in 21
23 (P → Q) → (¬P ∨ Q) add proposition defimpl1
24 (¬P ∨ Q) → (P → Q) add proposition defimpl2
25 (D → C) → ((¬(P ∨ (Q ∨ A)) ∨ D) → (¬(P ∨ (Q ∨ A)) ∨ C)) replace proposition variable B by ¬(P ∨ (Q ∨ A)) in 9
26 (D → ((Q ∨ (P ∨ A)) ∨ P)) → ((¬(P ∨ (Q ∨ A)) ∨ D) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) replace proposition variable C by (Q ∨ (P ∨ A)) ∨ P in 25
27 ((P ∨ (Q ∨ (P ∨ A))) → ((Q ∨ (P ∨ A)) ∨ P)) → ((¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) replace proposition variable D by P ∨ (Q ∨ (P ∨ A)) in 26
28 (¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)) modus ponens with 22, 27
29 (P → B) → (¬P ∨ B) replace proposition variable Q by B in 23
30 (C → B) → (¬C ∨ B) replace proposition variable P by C in 29
31 (C → (P ∨ (Q ∨ (P ∨ A)))) → (¬C ∨ (P ∨ (Q ∨ (P ∨ A)))) replace proposition variable B by P ∨ (Q ∨ (P ∨ A)) in 30
32 ((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A)))) replace proposition variable C by P ∨ (Q ∨ A) in 31
33 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
34 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 33
35 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 34
36 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 35
37 (D → C) → ((((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → D) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → C)) replace proposition variable B by (P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A))) in 36
38 (D → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) → ((((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → D) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)))) replace proposition variable C by ¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P) in 37
39 ((¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) → ((((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A))))) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)))) replace proposition variable D by ¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A))) in 38
40 (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ (P ∨ (Q ∨ (P ∨ A))))) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) modus ponens with 28, 39
41 ((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)) modus ponens with 32, 40
42 (¬P ∨ B) → (P → B) replace proposition variable Q by B in 24
43 (¬C ∨ B) → (C → B) replace proposition variable P by C in 42
44 (¬C ∨ ((Q ∨ (P ∨ A)) ∨ P)) → (C → ((Q ∨ (P ∨ A)) ∨ P)) replace proposition variable B by (Q ∨ (P ∨ A)) ∨ P in 43
45 (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)) replace proposition variable C by P ∨ (Q ∨ A) in 44
46 (D → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P))) → ((((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → D) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)))) replace proposition variable C by (P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P) in 37
47 ((¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P)) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P))) → ((((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)))) replace proposition variable D by ¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P) in 46
48 (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → (¬(P ∨ (Q ∨ A)) ∨ ((Q ∨ (P ∨ A)) ∨ P))) → (((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P))) modus ponens with 45, 47
49 ((P ∨ (Q ∨ A)) → (P ∨ (Q ∨ (P ∨ A)))) → ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)) modus ponens with 41, 48
50 (P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P) modus ponens with 17, 49
51 (P ∨ A) → (Q ∨ (P ∨ A)) replace proposition variable P by P ∨ A in 1
52 P → (P ∨ Q) add axiom axiom2
53 P → (P ∨ A) replace proposition variable Q by A in 52
54 (D → C) → ((P → D) → (P → C)) replace proposition variable B by P in 36
55 (D → (Q ∨ (P ∨ A))) → ((P → D) → (P → (Q ∨ (P ∨ A)))) replace proposition variable C by Q ∨ (P ∨ A) in 54
56 ((P ∨ A) → (Q ∨ (P ∨ A))) → ((P → (P ∨ A)) → (P → (Q ∨ (P ∨ A)))) replace proposition variable D by P ∨ A in 55
57 (P → (P ∨ A)) → (P → (Q ∨ (P ∨ A))) modus ponens with 51, 56
58 P → (Q ∨ (P ∨ A)) modus ponens with 53, 57
59 (D → C) → (((Q ∨ (P ∨ A)) ∨ D) → ((Q ∨ (P ∨ A)) ∨ C)) replace proposition variable B by Q ∨ (P ∨ A) in 9
60 (D → (Q ∨ (P ∨ A))) → (((Q ∨ (P ∨ A)) ∨ D) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) replace proposition variable C by Q ∨ (P ∨ A) in 59
61 (P → (Q ∨ (P ∨ A))) → (((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) replace proposition variable D by P in 60
62 ((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))) modus ponens with 58, 61
63 (P ∨ P) → P add proposition hilb11
64 (B ∨ B) → B replace proposition variable P by B in 63
65 ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))) → (Q ∨ (P ∨ A)) replace proposition variable B by Q ∨ (P ∨ A) in 64
66 (D → C) → ((¬((Q ∨ (P ∨ A)) ∨ P) ∨ D) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ C)) replace proposition variable B by ¬((Q ∨ (P ∨ A)) ∨ P) in 9
67 (D → (Q ∨ (P ∨ A))) → ((¬((Q ∨ (P ∨ A)) ∨ P) ∨ D) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) replace proposition variable C by Q ∨ (P ∨ A) in 66
68 (((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))) → (Q ∨ (P ∨ A))) → ((¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) replace proposition variable D by (Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)) in 67
69 (¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))) modus ponens with 65, 68
70 (C → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬C ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) replace proposition variable B by (Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)) in 30
71 (((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) replace proposition variable C by (Q ∨ (P ∨ A)) ∨ P in 70
72 (D → C) → (((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → D) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → C)) replace proposition variable B by ((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))) in 36
73 (D → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) → (((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → D) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))))) replace proposition variable C by ¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)) in 72
74 ((¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) → (((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))))) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))))) replace proposition variable D by ¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))) in 73
75 ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A))))) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) modus ponens with 69, 74
76 (((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))) modus ponens with 71, 75
77 (¬C ∨ (Q ∨ (P ∨ A))) → (C → (Q ∨ (P ∨ A))) replace proposition variable B by Q ∨ (P ∨ A) in 43
78 (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A))) replace proposition variable C by (Q ∨ (P ∨ A)) ∨ P in 77
79 (D → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A)))) → (((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → D) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A))))) replace proposition variable C by ((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A)) in 72
80 ((¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A)))) → (((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A))))) replace proposition variable D by ¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)) in 79
81 ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (¬((Q ∨ (P ∨ A)) ∨ P) ∨ (Q ∨ (P ∨ A)))) → ((((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A)))) modus ponens with 78, 80
82 (((Q ∨ (P ∨ A)) ∨ P) → ((Q ∨ (P ∨ A)) ∨ (Q ∨ (P ∨ A)))) → (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A))) modus ponens with 76, 81
83 ((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A)) modus ponens with 62, 82
84 (D → C) → (((P ∨ (Q ∨ A)) → D) → ((P ∨ (Q ∨ A)) → C)) replace proposition variable B by P ∨ (Q ∨ A) in 36
85 (D → (Q ∨ (P ∨ A))) → (((P ∨ (Q ∨ A)) → D) → ((P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)))) replace proposition variable C by Q ∨ (P ∨ A) in 84
86 (((Q ∨ (P ∨ A)) ∨ P) → (Q ∨ (P ∨ A))) → (((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)) → ((P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)))) replace proposition variable D by (Q ∨ (P ∨ A)) ∨ P in 85
87 ((P ∨ (Q ∨ A)) → ((Q ∨ (P ∨ A)) ∨ P)) → ((P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A))) modus ponens with 83, 86
88 (P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)) modus ponens with 50, 87
qed

The associative law for the disjunction (first direction):

20. Proposition
      (P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A)     (hilb14)

Proof:
1 (P ∨ Q) → (Q ∨ P) add proposition hilb9
2 (P ∨ B) → (B ∨ P) replace proposition variable Q by B in 1
3 (C ∨ B) → (B ∨ C) replace proposition variable P by C in 2
4 (C ∨ A) → (A ∨ C) replace proposition variable B by A in 3
5 (Q ∨ A) → (A ∨ Q) replace proposition variable C by Q in 4
6 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
7 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 6
8 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 7
9 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 8
10 (D → C) → ((P ∨ D) → (P ∨ C)) replace proposition variable B by P in 9
11 (D → (A ∨ Q)) → ((P ∨ D) → (P ∨ (A ∨ Q))) replace proposition variable C by A ∨ Q in 10
12 ((Q ∨ A) → (A ∨ Q)) → ((P ∨ (Q ∨ A)) → (P ∨ (A ∨ Q))) replace proposition variable D by Q ∨ A in 11
13 (P ∨ (Q ∨ A)) → (P ∨ (A ∨ Q)) modus ponens with 5, 12
14 (P → Q) → (¬P ∨ Q) add proposition defimpl1
15 (¬P ∨ Q) → (P → Q) add proposition defimpl2
16 (P → B) → (¬P ∨ B) replace proposition variable Q by B in 14
17 (C → B) → (¬C ∨ B) replace proposition variable P by C in 16
18 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
19 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 18
20 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 19
21 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 20
22 (¬P ∨ B) → (P → B) replace proposition variable Q by B in 15
23 (¬C ∨ B) → (C → B) replace proposition variable P by C in 22
24 (P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)) add proposition hilb13
25 (P ∨ (Q ∨ B)) → (Q ∨ (P ∨ B)) replace proposition variable A by B in 24
26 (P ∨ (C ∨ B)) → (C ∨ (P ∨ B)) replace proposition variable Q by C in 25
27 (D ∨ (C ∨ B)) → (C ∨ (D ∨ B)) replace proposition variable P by D in 26
28 (D ∨ (C ∨ Q)) → (C ∨ (D ∨ Q)) replace proposition variable B by Q in 27
29 (D ∨ (A ∨ Q)) → (A ∨ (D ∨ Q)) replace proposition variable C by A in 28
30 (P ∨ (A ∨ Q)) → (A ∨ (P ∨ Q)) replace proposition variable D by P in 29
31 (D → C) → (((P ∨ (Q ∨ A)) → D) → ((P ∨ (Q ∨ A)) → C)) replace proposition variable B by P ∨ (Q ∨ A) in 21
32 (D → (A ∨ (P ∨ Q))) → (((P ∨ (Q ∨ A)) → D) → ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q)))) replace proposition variable C by A ∨ (P ∨ Q) in 31
33 ((P ∨ (A ∨ Q)) → (A ∨ (P ∨ Q))) → (((P ∨ (Q ∨ A)) → (P ∨ (A ∨ Q))) → ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q)))) replace proposition variable D by P ∨ (A ∨ Q) in 32
34 ((P ∨ (Q ∨ A)) → (P ∨ (A ∨ Q))) → ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) modus ponens with 30, 33
35 (P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q)) modus ponens with 13, 34
36 (C ∨ (P ∨ Q)) → ((P ∨ Q) ∨ C) replace proposition variable B by P ∨ Q in 3
37 (A ∨ (P ∨ Q)) → ((P ∨ Q) ∨ A) replace proposition variable C by A in 36
38 (D → C) → ((¬(P ∨ (Q ∨ A)) ∨ D) → (¬(P ∨ (Q ∨ A)) ∨ C)) replace proposition variable B by ¬(P ∨ (Q ∨ A)) in 9
39 (D → ((P ∨ Q) ∨ A)) → ((¬(P ∨ (Q ∨ A)) ∨ D) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) replace proposition variable C by (P ∨ Q) ∨ A in 38
40 ((A ∨ (P ∨ Q)) → ((P ∨ Q) ∨ A)) → ((¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) replace proposition variable D by A ∨ (P ∨ Q) in 39
41 (¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)) modus ponens with 37, 40
42 (C → (A ∨ (P ∨ Q))) → (¬C ∨ (A ∨ (P ∨ Q))) replace proposition variable B by A ∨ (P ∨ Q) in 17
43 ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q))) replace proposition variable C by P ∨ (Q ∨ A) in 42
44 (D → C) → ((((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → D) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → C)) replace proposition variable B by (P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q)) in 21
45 (D → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) → ((((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → D) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)))) replace proposition variable C by ¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A) in 44
46 ((¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) → ((((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q)))) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)))) replace proposition variable D by ¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q)) in 45
47 (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ (A ∨ (P ∨ Q)))) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) modus ponens with 41, 46
48 ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)) modus ponens with 43, 47
49 (¬C ∨ ((P ∨ Q) ∨ A)) → (C → ((P ∨ Q) ∨ A)) replace proposition variable B by (P ∨ Q) ∨ A in 23
50 (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A)) replace proposition variable C by P ∨ (Q ∨ A) in 49
51 (D → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A))) → ((((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → D) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A)))) replace proposition variable C by (P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A) in 44
52 ((¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A)) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A))) → ((((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A)))) replace proposition variable D by ¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A) in 51
53 (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → (¬(P ∨ (Q ∨ A)) ∨ ((P ∨ Q) ∨ A))) → (((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A))) modus ponens with 50, 52
54 ((P ∨ (Q ∨ A)) → (A ∨ (P ∨ Q))) → ((P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A)) modus ponens with 48, 53
55 (P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A) modus ponens with 35, 54
qed

The associative law for the disjunction (second direction):

21. Proposition
      ((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))     (hilb15)

Proof:
1 (P ∨ (Q ∨ A)) → ((P ∨ Q) ∨ A) add proposition hilb14
2 (P ∨ (Q ∨ B)) → ((P ∨ Q) ∨ B) replace proposition variable A by B in 1
3 (P ∨ (C ∨ B)) → ((P ∨ C) ∨ B) replace proposition variable Q by C in 2
4 (D ∨ (C ∨ B)) → ((D ∨ C) ∨ B) replace proposition variable P by D in 3
5 (D ∨ (C ∨ P)) → ((D ∨ C) ∨ P) replace proposition variable B by P in 4
6 (D ∨ (Q ∨ P)) → ((D ∨ Q) ∨ P) replace proposition variable C by Q in 5
7 (A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P) replace proposition variable D by A in 6
8 (Q ∨ P) → (P ∨ Q) add proposition hilb10
9 (B ∨ P) → (P ∨ B) replace proposition variable Q by B in 8
10 (B ∨ C) → (C ∨ B) replace proposition variable P by C in 9
11 ((Q ∨ P) ∨ C) → (C ∨ (Q ∨ P)) replace proposition variable B by Q ∨ P in 10
12 ((Q ∨ P) ∨ A) → (A ∨ (Q ∨ P)) replace proposition variable C by A in 11
13 (P → Q) → (¬P ∨ Q) add proposition defimpl1
14 (¬P ∨ Q) → (P → Q) add proposition defimpl2
15 (P → Q) → (¬Q → ¬P) add proposition hilb7
16 (P → B) → (¬B → ¬P) replace proposition variable Q by B in 15
17 (C → B) → (¬B → ¬C) replace proposition variable P by C in 16
18 (C → (A ∨ (Q ∨ P))) → (¬(A ∨ (Q ∨ P)) → ¬C) replace proposition variable B by A ∨ (Q ∨ P) in 17
19 (((Q ∨ P) ∨ A) → (A ∨ (Q ∨ P))) → (¬(A ∨ (Q ∨ P)) → ¬((Q ∨ P) ∨ A)) replace proposition variable C by (Q ∨ P) ∨ A in 18
20 ¬(A ∨ (Q ∨ P)) → ¬((Q ∨ P) ∨ A) modus ponens with 12, 19
21 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
22 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 21
23 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 22
24 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 23
25 (D → C) → ((((A ∨ Q) ∨ P) ∨ D) → (((A ∨ Q) ∨ P) ∨ C)) replace proposition variable B by (A ∨ Q) ∨ P in 24
26 (D → ¬((Q ∨ P) ∨ A)) → ((((A ∨ Q) ∨ P) ∨ D) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) replace proposition variable C by ¬((Q ∨ P) ∨ A) in 25
27 (¬(A ∨ (Q ∨ P)) → ¬((Q ∨ P) ∨ A)) → ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) replace proposition variable D by ¬(A ∨ (Q ∨ P)) in 26
28 (((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) modus ponens with 20, 27
29 (P ∨ Q) → (Q ∨ P) add axiom axiom3
30 (P ∨ B) → (B ∨ P) replace proposition variable Q by B in 29
31 (C ∨ B) → (B ∨ C) replace proposition variable P by C in 30
32 (C ∨ ¬((Q ∨ P) ∨ A)) → (¬((Q ∨ P) ∨ A) ∨ C) replace proposition variable B by ¬((Q ∨ P) ∨ A) in 31
33 (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) replace proposition variable C by (A ∨ Q) ∨ P in 32
34 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
35 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 34
36 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 35
37 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 36
38 (D → C) → (((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → D) → ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → C)) replace proposition variable B by ((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P)) in 37
39 (D → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → D) → ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable C by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 38
40 ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) → ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable D by ((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A) in 39
41 ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) → ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) modus ponens with 33, 40
42 (((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) modus ponens with 28, 41
43 (C ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ C) replace proposition variable B by (A ∨ Q) ∨ P in 31
44 (¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) replace proposition variable C by ¬(A ∨ (Q ∨ P)) in 43
45 (D → C) → (((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → D) → ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → C)) replace proposition variable B by ¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P) in 37
46 (D → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → D) → ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable C by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 45
47 ((((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P))) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P)))) → ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable D by ((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P)) in 46
48 ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬(A ∨ (Q ∨ P)))) → ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) modus ponens with 42, 47
49 (¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) modus ponens with 44, 48
50 (P → B) → (¬P ∨ B) replace proposition variable Q by B in 13
51 (C → B) → (¬C ∨ B) replace proposition variable P by C in 50
52 (C → ((A ∨ Q) ∨ P)) → (¬C ∨ ((A ∨ Q) ∨ P)) replace proposition variable B by (A ∨ Q) ∨ P in 51
53 ((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) replace proposition variable C by A ∨ (Q ∨ P) in 52
54 (D → C) → ((((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → D) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → C)) replace proposition variable B by (A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P) in 37
55 (D → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → D) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable C by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 54
56 ((¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P))) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable D by ¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P) in 55
57 (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬(A ∨ (Q ∨ P)) ∨ ((A ∨ Q) ∨ P))) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) modus ponens with 49, 56
58 ((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) modus ponens with 53, 57
59 (¬P ∨ B) → (P → B) replace proposition variable Q by B in 14
60 (¬C ∨ B) → (C → B) replace proposition variable P by C in 59
61 (¬C ∨ ((A ∨ Q) ∨ P)) → (C → ((A ∨ Q) ∨ P)) replace proposition variable B by (A ∨ Q) ∨ P in 60
62 (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) replace proposition variable C by (Q ∨ P) ∨ A in 61
63 (D → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P))) → ((((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → D) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)))) replace proposition variable C by ((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P) in 54
64 ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P))) → ((((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)))) replace proposition variable D by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 63
65 (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P))) modus ponens with 62, 64
66 ((A ∨ (Q ∨ P)) → ((A ∨ Q) ∨ P)) → (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) modus ponens with 58, 65
67 ((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P) modus ponens with 7, 66
68 (D → C) → ((A ∨ D) → (A ∨ C)) replace proposition variable B by A in 24
69 (D → (Q ∨ P)) → ((A ∨ D) → (A ∨ (Q ∨ P))) replace proposition variable C by Q ∨ P in 68
70 ((P ∨ Q) → (Q ∨ P)) → ((A ∨ (P ∨ Q)) → (A ∨ (Q ∨ P))) replace proposition variable D by P ∨ Q in 69
71 (A ∨ (P ∨ Q)) → (A ∨ (Q ∨ P)) modus ponens with 29, 70
72 (C ∨ (Q ∨ P)) → ((Q ∨ P) ∨ C) replace proposition variable B by Q ∨ P in 31
73 (A ∨ (Q ∨ P)) → ((Q ∨ P) ∨ A) replace proposition variable C by A in 72
74 (D → C) → (((A ∨ (P ∨ Q)) → D) → ((A ∨ (P ∨ Q)) → C)) replace proposition variable B by A ∨ (P ∨ Q) in 37
75 (D → ((Q ∨ P) ∨ A)) → (((A ∨ (P ∨ Q)) → D) → ((A ∨ (P ∨ Q)) → ((Q ∨ P) ∨ A))) replace proposition variable C by (Q ∨ P) ∨ A in 74
76 ((A ∨ (Q ∨ P)) → ((Q ∨ P) ∨ A)) → (((A ∨ (P ∨ Q)) → (A ∨ (Q ∨ P))) → ((A ∨ (P ∨ Q)) → ((Q ∨ P) ∨ A))) replace proposition variable D by A ∨ (Q ∨ P) in 75
77 ((A ∨ (P ∨ Q)) → (A ∨ (Q ∨ P))) → ((A ∨ (P ∨ Q)) → ((Q ∨ P) ∨ A)) modus ponens with 73, 76
78 (A ∨ (P ∨ Q)) → ((Q ∨ P) ∨ A) modus ponens with 71, 77
79 (C ∨ A) → (A ∨ C) replace proposition variable B by A in 31
80 ((P ∨ Q) ∨ A) → (A ∨ (P ∨ Q)) replace proposition variable C by P ∨ Q in 79
81 (D → C) → ((((P ∨ Q) ∨ A) → D) → (((P ∨ Q) ∨ A) → C)) replace proposition variable B by (P ∨ Q) ∨ A in 37
82 (D → ((Q ∨ P) ∨ A)) → ((((P ∨ Q) ∨ A) → D) → (((P ∨ Q) ∨ A) → ((Q ∨ P) ∨ A))) replace proposition variable C by (Q ∨ P) ∨ A in 81
83 ((A ∨ (P ∨ Q)) → ((Q ∨ P) ∨ A)) → ((((P ∨ Q) ∨ A) → (A ∨ (P ∨ Q))) → (((P ∨ Q) ∨ A) → ((Q ∨ P) ∨ A))) replace proposition variable D by A ∨ (P ∨ Q) in 82
84 (((P ∨ Q) ∨ A) → (A ∨ (P ∨ Q))) → (((P ∨ Q) ∨ A) → ((Q ∨ P) ∨ A)) modus ponens with 78, 83
85 ((P ∨ Q) ∨ A) → ((Q ∨ P) ∨ A) modus ponens with 80, 84
86 (C → ((Q ∨ P) ∨ A)) → (¬((Q ∨ P) ∨ A) → ¬C) replace proposition variable B by (Q ∨ P) ∨ A in 17
87 (((P ∨ Q) ∨ A) → ((Q ∨ P) ∨ A)) → (¬((Q ∨ P) ∨ A) → ¬((P ∨ Q) ∨ A)) replace proposition variable C by (P ∨ Q) ∨ A in 86
88 ¬((Q ∨ P) ∨ A) → ¬((P ∨ Q) ∨ A) modus ponens with 85, 87
89 (D → ¬((P ∨ Q) ∨ A)) → ((((A ∨ Q) ∨ P) ∨ D) → (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A))) replace proposition variable C by ¬((P ∨ Q) ∨ A) in 25
90 (¬((Q ∨ P) ∨ A) → ¬((P ∨ Q) ∨ A)) → ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A))) replace proposition variable D by ¬((Q ∨ P) ∨ A) in 89
91 (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A)) modus ponens with 88, 90
92 (C ∨ ¬((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ C) replace proposition variable B by ¬((P ∨ Q) ∨ A) in 31
93 (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) replace proposition variable C by (A ∨ Q) ∨ P in 92
94 (D → C) → (((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → D) → ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → C)) replace proposition variable B by ((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A) in 37
95 (D → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → D) → ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable C by ¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P) in 94
96 ((((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A))) → ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable D by ((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A) in 95
97 ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (((A ∨ Q) ∨ P) ∨ ¬((P ∨ Q) ∨ A))) → ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) modus ponens with 93, 96
98 (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) modus ponens with 91, 97
99 (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) replace proposition variable C by ¬((Q ∨ P) ∨ A) in 43
100 (D → C) → (((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → D) → ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → C)) replace proposition variable B by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 37
101 (D → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → D) → ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable C by ¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P) in 100
102 ((((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) → ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable D by ((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A) in 101
103 ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((A ∨ Q) ∨ P) ∨ ¬((Q ∨ P) ∨ A))) → ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) modus ponens with 98, 102
104 (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) modus ponens with 99, 103
105 (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) replace proposition variable C by (Q ∨ P) ∨ A in 52
106 (D → C) → (((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → C)) replace proposition variable B by ((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P) in 37
107 (D → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable C by ¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P) in 106
108 ((¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → (((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)))) replace proposition variable D by ¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P) in 107
109 ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((Q ∨ P) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) modus ponens with 104, 108
110 (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) modus ponens with 105, 109
111 (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) replace proposition variable C by (P ∨ Q) ∨ A in 61
112 (D → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P))) → (((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)))) replace proposition variable C by ((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P) in 106
113 ((¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P))) → (((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)))) replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P) in 112
114 ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P))) modus ponens with 111, 113
115 (((Q ∨ P) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) modus ponens with 110, 114
116 ((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P) modus ponens with 67, 115
117 (C ∨ P) → (P ∨ C) replace proposition variable B by P in 31
118 ((A ∨ Q) ∨ P) → (P ∨ (A ∨ Q)) replace proposition variable C by A ∨ Q in 117
119 (D → C) → ((¬((P ∨ Q) ∨ A) ∨ D) → (¬((P ∨ Q) ∨ A) ∨ C)) replace proposition variable B by ¬((P ∨ Q) ∨ A) in 24
120 (D → (P ∨ (A ∨ Q))) → ((¬((P ∨ Q) ∨ A) ∨ D) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) replace proposition variable C by P ∨ (A ∨ Q) in 119
121 (((A ∨ Q) ∨ P) → (P ∨ (A ∨ Q))) → ((¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) replace proposition variable D by (A ∨ Q) ∨ P in 120
122 (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) modus ponens with 118, 121
123 (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) replace proposition variable C by (P ∨ Q) ∨ A in 52
124 (D → C) → (((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → C)) replace proposition variable B by ((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P) in 37
125 (D → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → (((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))))) replace proposition variable C by ¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)) in 124
126 ((¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → (((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))))) replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P) in 125
127 ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ ((A ∨ Q) ∨ P))) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) modus ponens with 122, 126
128 (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) modus ponens with 123, 127
129 (¬C ∨ (P ∨ (A ∨ Q))) → (C → (P ∨ (A ∨ Q))) replace proposition variable B by P ∨ (A ∨ Q) in 60
130 (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) replace proposition variable C by (P ∨ Q) ∨ A in 129
131 (D → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)))) → (((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → D) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))))) replace proposition variable C by ((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)) in 124
132 ((¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)))) → (((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))))) replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)) in 131
133 ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → ((((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)))) modus ponens with 130, 132
134 (((P ∨ Q) ∨ A) → ((A ∨ Q) ∨ P)) → (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) modus ponens with 128, 133
135 ((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)) modus ponens with 116, 134
136 (C ∨ Q) → (Q ∨ C) replace proposition variable B by Q in 31
137 (A ∨ Q) → (Q ∨ A) replace proposition variable C by A in 136
138 (D → C) → ((P ∨ D) → (P ∨ C)) replace proposition variable B by P in 24
139 (D → (Q ∨ A)) → ((P ∨ D) → (P ∨ (Q ∨ A))) replace proposition variable C by Q ∨ A in 138
140 ((A ∨ Q) → (Q ∨ A)) → ((P ∨ (A ∨ Q)) → (P ∨ (Q ∨ A))) replace proposition variable D by A ∨ Q in 139
141 (P ∨ (A ∨ Q)) → (P ∨ (Q ∨ A)) modus ponens with 137, 140
142 (D → (P ∨ (Q ∨ A))) → ((¬((P ∨ Q) ∨ A) ∨ D) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) replace proposition variable C by P ∨ (Q ∨ A) in 119
143 ((P ∨ (A ∨ Q)) → (P ∨ (Q ∨ A))) → ((¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) replace proposition variable D by P ∨ (A ∨ Q) in 142
144 (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))) modus ponens with 141, 143
145 (C → (P ∨ (A ∨ Q))) → (¬C ∨ (P ∨ (A ∨ Q))) replace proposition variable B by P ∨ (A ∨ Q) in 51
146 (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) replace proposition variable C by (P ∨ Q) ∨ A in 145
147 (D → C) → (((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → D) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → C)) replace proposition variable B by ((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q)) in 37
148 (D → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) → (((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → D) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))))) replace proposition variable C by ¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)) in 147
149 ((¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) → (((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))))) replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)) in 148
150 ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (A ∨ Q)))) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) modus ponens with 144, 149
151 (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))) modus ponens with 146, 150
152 (¬C ∨ (P ∨ (Q ∨ A))) → (C → (P ∨ (Q ∨ A))) replace proposition variable B by P ∨ (Q ∨ A) in 60
153 (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))) replace proposition variable C by (P ∨ Q) ∨ A in 152
154 (D → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)))) → (((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → D) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))))) replace proposition variable C by ((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)) in 147
155 ((¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)))) → (((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))))) replace proposition variable D by ¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)) in 154
156 ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (¬((P ∨ Q) ∨ A) ∨ (P ∨ (Q ∨ A)))) → ((((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)))) modus ponens with 153, 155
157 (((P ∨ Q) ∨ A) → (P ∨ (A ∨ Q))) → (((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A))) modus ponens with 151, 156
158 ((P ∨ Q) ∨ A) → (P ∨ (Q ∨ A)) modus ponens with 135, 157
qed

Another consequence from hilb13 is the exchange of preconditions:

22. Proposition
      (P → (Q → A)) → (Q → (P → A))     (hilb16)

Proof:
1 (P ∨ (Q ∨ A)) → (Q ∨ (P ∨ A)) add proposition hilb13
2 (P ∨ (Q ∨ B)) → (Q ∨ (P ∨ B)) replace proposition variable A by B in 1
3 (P ∨ (C ∨ B)) → (C ∨ (P ∨ B)) replace proposition variable Q by C in 2
4 (D ∨ (C ∨ B)) → (C ∨ (D ∨ B)) replace proposition variable P by D in 3
5 (D ∨ (C ∨ A)) → (C ∨ (D ∨ A)) replace proposition variable B by A in 4
6 (D ∨ (¬Q ∨ A)) → (¬Q ∨ (D ∨ A)) replace proposition variable C by ¬Q in 5
7 (¬P ∨ (¬Q ∨ A)) → (¬Q ∨ (¬P ∨ A)) replace proposition variable D by ¬P in 6
8 (P → (¬Q ∨ A)) → (¬Q ∨ (¬P ∨ A)) reverse abbreviation impl in 7 at occurence 1
9 (P → (Q → A)) → (¬Q ∨ (¬P ∨ A)) reverse abbreviation impl in 8 at occurence 1
10 (P → (Q → A)) → (Q → (¬P ∨ A)) reverse abbreviation impl in 9 at occurence 1
11 (P → (Q → A)) → (Q → (P → A)) reverse abbreviation impl in 10 at occurence 1
qed

An analogus form for hyperref [hilb16]hilb16:

23. Proposition
      (Q → (P → A)) → (P → (Q → A))     (hilb17)

Proof:
1 (P → (Q → A)) → (Q → (P → A)) add proposition hilb16
2 (P → (Q → B)) → (Q → (P → B)) replace proposition variable A by B in 1
3 (P → (C → B)) → (C → (P → B)) replace proposition variable Q by C in 2
4 (D → (C → B)) → (C → (D → B)) replace proposition variable P by D in 3
5 (D → (C → A)) → (C → (D → A)) replace proposition variable B by A in 4
6 (D → (P → A)) → (P → (D → A)) replace proposition variable C by P in 5
7 (Q → (P → A)) → (P → (Q → A)) replace proposition variable D by Q in 6
qed

Cross References

This document is used by the following documents: