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