# Some more theorems of Predicate Calculus

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

## Description

This module includes first proofs of predicate calculus theorems.

## References

This document uses the results of the following documents:

## Content

A simple implication:

1. Proposition
∀x R(x) → ∃x R(x)     (predtheo1)

Proof:
 1 ∀x R(x) → R(y) add axiom axiom5 2 R(y) → ∃x R(x) add axiom axiom6 3 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1 4 (B → Q) → ((A → B) → (A → Q)) replace proposition variable P by B in 3 5 (B → C) → ((A → B) → (A → C)) replace proposition variable Q by C in 4 6 (B → C) → ((D → B) → (D → C)) replace proposition variable A by D in 5 7 (R(y) → C) → ((D → R(y)) → (D → C)) replace proposition variable B by R(y) in 6 8 (R(y) → ∃x R(x)) → ((D → R(y)) → (D → ∃x R(x))) replace proposition variable C by ∃x R(x) in 7 9 (R(y) → ∃x R(x)) → ((∀x R(x) → R(y)) → (∀x R(x) → ∃x R(x))) replace proposition variable D by ∀x R(x) in 8 10 (∀x R(x) → R(y)) → (∀x R(x) → ∃x R(x)) modus ponens with 2, 9 11 ∀x R(x) → ∃x R(x) modus ponens with 1, 10 qed

A well known implication:

2. Proposition
∃x R(x) → ¬∀x ¬R(x)     (predtheo2)

Proof:
 1 ∀x R(x) → R(y) add axiom axiom5 2 ∀x ¬R(x) → ¬R(y) replace predicate variable R(@S1) by ¬R(@S1) in 1 3 ¬∀x ¬R(x) ∨ ¬R(y) use abbreviation impl in 2 at occurence 1 4 (P ∨ Q) → (Q ∨ P) add axiom axiom3 5 (¬∀x ¬R(x) ∨ Q) → (Q ∨ ¬∀x ¬R(x)) replace proposition variable P by ¬∀x ¬R(x) in 4 6 (¬∀x ¬R(x) ∨ ¬R(y)) → (¬R(y) ∨ ¬∀x ¬R(x)) replace proposition variable Q by ¬R(y) in 5 7 ¬R(y) ∨ ¬∀x ¬R(x) modus ponens with 3, 6 8 R(y) → ¬∀x ¬R(x) reverse abbreviation impl in 7 at occurence 1 9 ∃y R(y) → ¬∀x ¬R(x) particularization by y in 8 10 ∃x R(x) → ¬∀x ¬R(x) rename bound variable y into x in 9 at occurence 1 qed

The reverse is also true:

3. Proposition
¬∀x ¬R(x) → ∃x R(x)     (predtheo3)

Proof:
 1 R(y) → ∃x R(x) add axiom axiom6 2 (P → Q) → (¬Q → ¬P) add proposition hilb7 3 (A → Q) → (¬Q → ¬A) replace proposition variable P by A in 2 4 (A → B) → (¬B → ¬A) replace proposition variable Q by B in 3 5 (R(y) → B) → (¬B → ¬R(y)) replace proposition variable A by R(y) in 4 6 (R(y) → ∃x R(x)) → (¬∃x R(x) → ¬R(y)) replace proposition variable B by ∃x R(x) in 5 7 ¬∃x R(x) → ¬R(y) modus ponens with 1, 6 8 ¬∃x R(x) → ∀y ¬R(y) generalization by y in 7 9 (¬∃x R(x) → B) → (¬B → ¬¬∃x R(x)) replace proposition variable A by ¬∃x R(x) in 4 10 (¬∃x R(x) → ∀y ¬R(y)) → (¬∀y ¬R(y) → ¬¬∃x R(x)) replace proposition variable B by ∀y ¬R(y) in 9 11 ¬∀y ¬R(y) → ¬¬∃x R(x) modus ponens with 8, 10 12 ¬¬P → P add proposition hilb6 13 ¬¬Q → Q replace proposition variable P by Q in 12 14 ¬¬∃x R(x) → ∃x R(x) replace proposition variable Q by ∃x R(x) in 13 15 (P → Q) → (¬P ∨ Q) add proposition defimpl1 16 (¬P ∨ Q) → (P → Q) add proposition defimpl2 17 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4 18 (B → Q) → ((A ∨ B) → (A ∨ Q)) replace proposition variable P by B in 17 19 (B → C) → ((A ∨ B) → (A ∨ C)) replace proposition variable Q by C in 18 20 (B → C) → ((D ∨ B) → (D ∨ C)) replace proposition variable A by D in 19 21 (¬¬∃x R(x) → C) → ((D ∨ ¬¬∃x R(x)) → (D ∨ C)) replace proposition variable B by ¬¬∃x R(x) in 20 22 (¬¬∃x R(x) → ∃x R(x)) → ((D ∨ ¬¬∃x R(x)) → (D ∨ ∃x R(x))) replace proposition variable C by ∃x R(x) in 21 23 (¬¬∃x R(x) → ∃x R(x)) → ((¬¬∀y ¬R(y) ∨ ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ∃x R(x))) replace proposition variable D by ¬¬∀y ¬R(y) in 22 24 (¬¬∀y ¬R(y) ∨ ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ∃x R(x)) modus ponens with 14, 23 25 (A → Q) → (¬A ∨ Q) replace proposition variable P by A in 15 26 (A → B) → (¬A ∨ B) replace proposition variable Q by B in 25 27 (¬∀y ¬R(y) → B) → (¬¬∀y ¬R(y) ∨ B) replace proposition variable A by ¬∀y ¬R(y) in 26 28 (¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ¬¬∃x R(x)) replace proposition variable B by ¬¬∃x R(x) in 27 29 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1 30 (B → Q) → ((A → B) → (A → Q)) replace proposition variable P by B in 29 31 (B → C) → ((A → B) → (A → C)) replace proposition variable Q by C in 30 32 (B → C) → ((D → B) → (D → C)) replace proposition variable A by D in 31 33 ((¬¬∀y ¬R(y) ∨ ¬¬∃x R(x)) → C) → ((D → (¬¬∀y ¬R(y) ∨ ¬¬∃x R(x))) → (D → C)) replace proposition variable B by ¬¬∀y ¬R(y) ∨ ¬¬∃x R(x) in 32 34 ((¬¬∀y ¬R(y) ∨ ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ∃x R(x))) → ((D → (¬¬∀y ¬R(y) ∨ ¬¬∃x R(x))) → (D → (¬¬∀y ¬R(y) ∨ ∃x R(x)))) replace proposition variable C by ¬¬∀y ¬R(y) ∨ ∃x R(x) in 33 35 ((¬¬∀y ¬R(y) ∨ ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ∃x R(x))) → (((¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ¬¬∃x R(x))) → ((¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ∃x R(x)))) replace proposition variable D by ¬∀y ¬R(y) → ¬¬∃x R(x) in 34 36 ((¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ¬¬∃x R(x))) → ((¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ∃x R(x))) modus ponens with 24, 35 37 (¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ∃x R(x)) modus ponens with 28, 36 38 (¬A ∨ Q) → (A → Q) replace proposition variable P by A in 16 39 (¬A ∨ B) → (A → B) replace proposition variable Q by B in 38 40 (¬¬∀y ¬R(y) ∨ B) → (¬∀y ¬R(y) → B) replace proposition variable A by ¬∀y ¬R(y) in 39 41 (¬¬∀y ¬R(y) ∨ ∃x R(x)) → (¬∀y ¬R(y) → ∃x R(x)) replace proposition variable B by ∃x R(x) in 40 42 ((¬¬∀y ¬R(y) ∨ ∃x R(x)) → C) → ((D → (¬¬∀y ¬R(y) ∨ ∃x R(x))) → (D → C)) replace proposition variable B by ¬¬∀y ¬R(y) ∨ ∃x R(x) in 32 43 ((¬¬∀y ¬R(y) ∨ ∃x R(x)) → (¬∀y ¬R(y) → ∃x R(x))) → ((D → (¬¬∀y ¬R(y) ∨ ∃x R(x))) → (D → (¬∀y ¬R(y) → ∃x R(x)))) replace proposition variable C by ¬∀y ¬R(y) → ∃x R(x) in 42 44 ((¬¬∀y ¬R(y) ∨ ∃x R(x)) → (¬∀y ¬R(y) → ∃x R(x))) → (((¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ∃x R(x))) → ((¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬∀y ¬R(y) → ∃x R(x)))) replace proposition variable D by ¬∀y ¬R(y) → ¬¬∃x R(x) in 43 45 ((¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬¬∀y ¬R(y) ∨ ∃x R(x))) → ((¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬∀y ¬R(y) → ∃x R(x))) modus ponens with 41, 44 46 (¬∀y ¬R(y) → ¬¬∃x R(x)) → (¬∀y ¬R(y) → ∃x R(x)) modus ponens with 37, 45 47 ¬∀y ¬R(y) → ∃x R(x) modus ponens with 11, 46 48 ¬∀x ¬R(x) → ∃x R(x) rename bound variable y into x in 47 at occurence 1 qed

Exchange of universal quantors:

4. Proposition
∀x ∀y R(x, y) → ∀y ∀x R(x, y)     (predtheo4)

Proof:
 1 ∀x R(x) → R(y) add axiom axiom5 2 ∀x R(x) → R(w) rename free variable y into w in 1 3 ∀r R(r) → R(w) rename bound variable x into r in 2 at occurence 1 4 ∀r R(r) → R(u) rename free variable w into u in 3 5 ∀y R(y) → R(u) rename bound variable r into y in 4 at occurence 1 6 ∀y R(z, y) → R(z, u) replace predicate variable R(@S1) by R(z, @S1) in 5 7 ∀x R(x) → R(r) rename free variable y into r in 1 8 ∀s R(s) → R(r) rename bound variable x into s in 7 at occurence 1 9 ∀s R(s) → R(z) rename free variable r into z in 8 10 ∀v R(v) → R(z) rename bound variable s into v in 9 at occurence 1 11 ∀v ∀w R(v, w) → ∀w R(z, w) replace predicate variable R(@S1) by ∀w R(@S1, w) in 10 12 ∀c ∀w R(c, w) → ∀w R(z, w) rename bound variable v into c in 11 at occurence 1 13 ∀c ∀d R(c, d) → ∀w R(z, w) rename bound variable w into d in 12 at occurence 1 14 ∀c ∀d R(c, d) → ∀x14 R(z, x14) rename bound variable w into x14 in 13 at occurence 1 15 ∀x ∀d R(x, d) → ∀x14 R(z, x14) rename bound variable c into x in 14 at occurence 1 16 ∀x ∀y R(x, y) → ∀x14 R(z, x14) rename bound variable d into y in 15 at occurence 1 17 ∀x ∀y R(x, y) → ∀y R(z, y) rename bound variable x14 into y in 16 at occurence 1 18 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1 19 (C → Q) → ((A → C) → (A → Q)) replace proposition variable P by C in 18 20 (C → D) → ((A → C) → (A → D)) replace proposition variable Q by D in 19 21 (C → D) → ((P7 → C) → (P7 → D)) replace proposition variable A by P7 in 20 22 (∀y R(z, y) → D) → ((P7 → ∀y R(z, y)) → (P7 → D)) replace proposition variable C by ∀y R(z, y) in 21 23 (∀y R(z, y) → R(z, u)) → ((P7 → ∀y R(z, y)) → (P7 → R(z, u))) replace proposition variable D by R(z, u) in 22 24 (∀y R(z, y) → R(z, u)) → ((∀x ∀y R(x, y) → ∀y R(z, y)) → (∀x ∀y R(x, y) → R(z, u))) replace proposition variable P7 by ∀x ∀y R(x, y) in 23 25 (∀x ∀y R(x, y) → ∀y R(z, y)) → (∀x ∀y R(x, y) → R(z, u)) modus ponens with 6, 24 26 ∀x ∀y R(x, y) → R(z, u) modus ponens with 17, 25 27 ∀x ∀y R(x, y) → ∀z R(z, u) generalization by z in 26 28 ∀x ∀y R(x, y) → ∀u ∀z R(z, u) generalization by u in 27 29 ∀x ∀y R(x, y) → ∀y ∀z R(z, y) rename bound variable u into y in 28 at occurence 1 30 ∀x ∀y R(x, y) → ∀y ∀x R(x, y) rename bound variable z into x in 29 at occurence 1 qed

Implication of changing sequence of existence and universal quantor:

5. Proposition
∃x ∀y R(x, y) → ∀y ∃x R(x, y)     (predtheo5)

Proof:
 1 ∀x R(x) → R(y) add axiom axiom5 2 ∀x R(x) → R(w) rename free variable y into w in 1 3 ∀r R(r) → R(w) rename bound variable x into r in 2 at occurence 1 4 ∀r R(r) → R(u) rename free variable w into u in 3 5 ∀y R(y) → R(u) rename bound variable r into y in 4 at occurence 1 6 ∀y R(x, y) → R(x, u) replace predicate variable R(@S1) by R(x, @S1) in 5 7 R(y) → ∃x R(x) add axiom axiom6 8 R(v) → ∃x R(x) rename free variable y into v in 7 9 R(v) → ∃w R(w) rename bound variable x into w in 8 at occurence 1 10 R(x) → ∃w R(w) rename free variable v into x in 9 11 R(x) → ∃z R(z) rename bound variable w into z in 10 at occurence 1 12 R(x, u) → ∃z R(z, u) replace predicate variable R(@S1) by R(@S1, u) in 11 13 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1 14 (C → Q) → ((A → C) → (A → Q)) replace proposition variable P by C in 13 15 (C → D) → ((A → C) → (A → D)) replace proposition variable Q by D in 14 16 (C → D) → ((P7 → C) → (P7 → D)) replace proposition variable A by P7 in 15 17 (R(x, u) → D) → ((P7 → R(x, u)) → (P7 → D)) replace proposition variable C by R(x, u) in 16 18 (R(x, u) → ∃z R(z, u)) → ((P7 → R(x, u)) → (P7 → ∃z R(z, u))) replace proposition variable D by ∃z R(z, u) in 17 19 (R(x, u) → ∃z R(z, u)) → ((∀y R(x, y) → R(x, u)) → (∀y R(x, y) → ∃z R(z, u))) replace proposition variable P7 by ∀y R(x, y) in 18 20 (∀y R(x, y) → R(x, u)) → (∀y R(x, y) → ∃z R(z, u)) modus ponens with 12, 19 21 ∀y R(x, y) → ∃z R(z, u) modus ponens with 6, 20 22 ∃x ∀y R(x, y) → ∃z R(z, u) particularization by x in 21 23 ∃x ∀y R(x, y) → ∀u ∃z R(z, u) generalization by u in 22 24 ∃x ∀y R(x, y) → ∀c ∃z R(z, c) rename bound variable u into c in 23 at occurence 1 25 ∃x ∀y R(x, y) → ∀c ∃d R(d, c) rename bound variable z into d in 24 at occurence 1 26 ∃x ∀y R(x, y) → ∀y ∃d R(d, y) rename bound variable c into y in 25 at occurence 1 27 ∃x ∀y R(x, y) → ∀y ∃x R(x, y) rename bound variable d into x in 26 at occurence 1 qed