{{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.

## Detachment

We have already encountered our first detachment rule, applyModusPonens, which takes a proposition and an implication with that proposition as antecedent.

### Multiple antecedents

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.

• p, (→ (∧ p q) r)(→ q r) (detach1of2)
• q, (→ (∧ p q) r)(→ p r) (detach2of2)
• p, (→ (∧ (∧ p q) r) consequent)(→ (∧ q r) consequent) (detach1of3)
• q, (→ (∧ (∧ p q) r) consequent)(→ (∧ p r) consequent) (detach2of3)
• p, (→ (∧ (∧ (∧ p q) r) s) consequent)(→ (∧ (∧ q r) s) consequent) (detach1of4)

### Nested formulas

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.

### Negated detachment

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.

## Transforming parts of formula

By "transforming", we mean applying a biconditional to replace part of a formula.

## More relationships between connectives

### Conjunction and implication

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>

### Negation and biconditional

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).

### Building in the consequent

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.

## Additional theorems in the consequent

The various *InConsequent theorems are generally easy consequences of composeConjunction.

## Theorems in the antecedent

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.

• (→ (→ p (→ q r)) consequent)(→ (→ (∧ p q) r) consequent) (importInAntecedent)
• (→ (→ (∧ p q) r) consequent)(→ (→ p (→ q r)) consequent) (exportInAntecedent)

## Rules for associativity

Here are some rules for changing the associativity in the consequent.

## Combinations of commutativity and associativity

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>

• (↔ (∧ (∧ p q) (∧ r s)) (∧ (∧ p r) (∧ q s))) (Conjunction4)

## Proof by contradiction

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.

## Done

We now export Interface:Classical propositional calculus.

<references/>