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