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