# 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