# Some more theorems of Predicate Calculus

name: predtheo2, module version: 1.00.00, rule version: 1.02.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 (" x (R(x)) ® \$ x (R(x))) hypothetical syllogism with 1 and 2 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 (Ø\$ x (R(x)) ® ØR(y)) apply proposition hilb7 in 1 3 (Ø\$ x (R(x)) ® " y (ØR(y))) generalization by y in 2 4 (Ø" y (ØR(y)) ® ØØ\$ x (R(x))) apply proposition hilb7 in 3 5 (Ø" y (ØR(y)) ® \$ x (R(x))) elementary equivalence in 4 at 1 of hilb6 with hilb5 6 (Ø" x (ØR(x)) ® \$ x (R(x))) rename bound variable y into x in 5 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 (" y (R(y)) ® R(u)) substitute variables in 1 3 (" y (R(z, y)) ® R(z, u)) replace predicate variable R(@S1) by R(z, @S1) in 2 4 (" v (R(v)) ® R(z)) substitute variables in 1 5 (" v (" w (R(v, w))) ® " w (R(z, w))) replace predicate variable R(@S1) by " w (R(@S1, w)) in 4 6 (" x (" y (R(x, y))) ® " y (R(z, y))) substitute variables in 5 7 (" x (" y (R(x, y))) ® R(z, u)) hypothetical syllogism with 6 and 3 8 (" x (" y (R(x, y))) ® " z (R(z, u))) generalization by z in 7 9 (" x (" y (R(x, y))) ® " u (" z (R(z, u)))) generalization by u in 8 10 (" x (" y (R(x, y))) ® " y (" z (R(z, y)))) rename bound variable u into y in 9 at occurence 1 11 (" x (" y (R(x, y))) ® " y (" x (R(x, y)))) rename bound variable z into x in 10 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 (" y (R(y)) ® R(u)) substitute variables in 1 3 (" y (R(x, y)) ® R(x, u)) replace predicate variable R(@S1) by R(x, @S1) in 2 4 (R(y) ® \$ x (R(x))) add axiom axiom6 5 (R(x) ® \$ z (R(z))) substitute variables in 4 6 (R(x, u) ® \$ z (R(z, u))) replace predicate variable R(@S1) by R(@S1, u) in 5 7 (" y (R(x, y)) ® \$ z (R(z, u))) hypothetical syllogism with 3 and 6 8 (\$ x (" y (R(x, y))) ® \$ z (R(z, u))) particularization by x in 7 9 (\$ x (" y (R(x, y))) ® " u (\$ z (R(z, u)))) generalization by u in 8 10 (\$ x (" y (R(x, y))) ® " y (\$ x (R(x, y)))) substitute variables in 9 qed