# 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