# First theorems of Predicate Calculus

name: predtheo1, module version: 1.00.00, rule version: 1.00.00, original: predtheo1, 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

First we prove a simple implication:

1. Proposition
∃x R(x) → ¬∀x ¬R(x)     (theo1)

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