Principia Mathematica II
Subject: Proof Methods Version Overview
Date: 2003-11-24
***********************************************************************
Prototype Warning
=================
This program suite is only a working prototype for the main project
*Hilbert II*. It concentrates on the basic logic foundation of
mathematics. The software design of the main implementation will be
highly different. The following information is only appropriate for
this prototype. Look at
http://www.qedeq.org/
http://sourceforge.net/projects/pmii/
to get the latest source code and information.
Rule Version Overview
=====================
The proof methods are listed in dependency from their version number.
The basic proof methods are those of Version 1.00.00. All other
versions of proof methods could be derived from the basic rules
together with the axioms of predicate calculus.
Rule Description
Version 1.00.00
ADDAXIOM add previous axiom to proof lines
ADDSENTENCE add previous proposition to proof lines
GENERALIZATION generalize a formula
MODUSPONENS use modus ponens
PARTICULARIZATION particularize a formula
RENAMEBOUNDVARIABLE rename a bound subject variable
RENAMEFREEVARIABLE rename a free subject variable
REPLACEPREDICATE replace predicate variable
REPLACEPROP replace proposition variable by formula
USEABBREVIATION use previous abbreviation
REVERSEABBREVIATION unuse previous abbreviation
Version 1.01.00
SUBSTLINE substitute various variables of a proof line
Version 1.01.01
APPLYAXIOM add axiom, substitute, use modus ponens
APPLYSENTENCE add proposition, subsitute, use modus ponens
Version 1.01.02
HYPOTHETICALSYLLOGISM use hypothetical syllogism
Version 1.01.03
RIGHTADDITION right addition of disjunction to implication
Version 1.01.04
LEFTADDITION left addition of disjunction to implication
REVERSEIMPLICATION build correct reversion of an implication
Version 1.01.05
LEFTADDITIONCONJUNCTION left addition of conjunction to implication
RIGHTADDITIONCONJUNCTION right addition of conjunction to implication
LEFTADDITIONIMPLICATION left addition of implication to implication
RIGHTADDITIONIMPLICATION right addition of implication to implication
Version 1.01.06
LEFTADDITIONEQUIVALENCE left addition of equivalence to implication
RIGHTADDITIONEQUIVALENCE right addition of equivalence to implication
Version 1.02.00
IMPLICATIONEQUIVALENT if two formulas impies each other any
occurence of one formula could be replaced
by the other one
Version 1.02.01
CONJUNCTION conjunction of two proved formulas