for questions or link request: module admin

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