{{header | title = Convenience theorems of | subtitle = propositional logic | left = | right = | shortcut = | notes = This page proves those statments of Interface:Classical propositional calculus which aren't in Interface:Principia Mathematica propositional logic theorems. This includes chiefly additional builders (which aren't necessarily in most textbook treatments as they take substitution for granted), additional variants on modus ponens and related theorems, and the like. Some of them are significant aids to making proofs concise and readable, but some of them are more arguable and are here to ease translating proofs from other systems or so that people writing proofs can make their own decisions. }} {{interfaces | imports = Interface:Principia Mathematica propositional logic theorems | exports = Interface:Classical propositional calculus }}
We first import Interface:Principia Mathematica propositional logic theorems:
As usual, p, q, and r are formulas. We also define some longer names which will make the formulas with a lot of variables more readable.
We have already encountered our first detachment rule, applyModusPonens, which takes a proposition and an implication with that proposition as antecedent.
This section is for variants in which the implication has several antecedents (that is, the antecedent is a conjunction of two or more propositions) and we detach one or more of the antecedents.
Here the "implication" is really a nesting of implications and/or biconditionals, and we detach one of the formulas from somewhere inside the nested formulas.
This variant of ''modus tollens'' detaches the right hand side of a biconditional, which is a consequent.<ref>[http://us.metamath.org/mpeuni/mtbiri.html mtbiri], metamath's set.mm, accessed July 20, 2010</ref>
Here's the same thing for the left side of the biconditional.
Here's one for two implications.
By "transforming", we mean applying a biconditional to replace part of a formula.
The following relationships between conjunction and implication parallel those between disjunction and implication (and in fact follow easily from them and DeMorgan's laws).<ref>ConjunctionImplication is *4.63 in ''Principia'', with the two sides of the biconditional commuted</ref>
Here we prove that ¬ p ↔ (p ↔ ⊥).
The builders in Interface:Principia Mathematica propositional logic theorems for the various connectives often have a theorem form (e.g. ConjunctionFunction) and a rule form (e.g. buildConjunction). They may have a version for the implication rather than the biconditional (e.g. DisjunctionSummation, although sometimes only the biconditionalized version holds) and variants which add a common formula to one side or the other (e.g. DisjunctionSummationLL and DisjunctionSummationRR). Here we prove some of those variations which we haven't proved yet. The LR and RL variations (analogous to DisjunctionSummationLR and DisjunctionSummationRL) haven't as often been needed, but they could go here too, if there is a need.
For implications, we call the two sides the antecedent and consequent, rather than L and R (well, except for theorems which were named before this convention was establish and which noone has gotten around to renaming yet).
Often we work with formulas which all have an antecedent in common, and in which all our building happens in the consequent. This is particularly helpful when dealing with substitution as it is handled in Interface:First-order logic with quantifiability.
The various *InConsequent theorems are generally easy consequences of composeConjunction.
There are more cases where it is convenient to have a rule that operates in the consequent than in the antecedent. But there are a few for the latter.
Here are some rules for changing the associativity in the consequent.
Commutativity and associativity might be combined in any number of ways, but a few patterns turn out to be common.
The first one swaps the second and third disjuncts in a disjunction of four formulas.<ref>[http://us.metamath.org/mpeuni/or4.html or4], metamath's set.mm, accessed February 5, 2011</ref>
The next theorem swaps the second and third conjuncts in a conjunction of four formulas.<ref>[http://us.metamath.org/mpeuni/an4.html an4], metamath's set.mm, accessed February 5, 2011</ref>
Although the theorems presented thus far do provide ways to make deductions concerning contradictions, the usual form of a proof by contradiction is either to assume a statement and proof its negation, or the other way around.
We now export Interface:Classical propositional calculus.
<references/>