for questions or link request: module admin

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