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, orignal: predtheo2, author of this module: Michael Meyling

Description

This module includes first proofs of predicate calculus theorems.

Uses the following modules:


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 seqence 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