for questions or link request: module admin

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