for questions or link request: module admin

Some more theorems of Predicate Calculus

name: predtheo2, module version: 1.00.00, rule version: 1.02.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 (" 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 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 (" 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