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: