# First theorems of Predicate Calculus

name: predtheo1, module version: 1.00.00, rule version: 1.00.00, orignal: predtheo1, author of this module: Michael Meyling

## Description

This module includes first proofs of predicate calculus theorems.

Uses the following modules:

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