# 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