Interface:Classical propositional calculus

From Wikiproofs
Jump to: navigation, search
Classical propositional calculus
This interface collects all important theorems from classical propositional calculus. It is meant as a user-friendly reservoir for those interfaces and proof modules which merely use propositional logic, without proving anything new within it.

Statements can be added if necessary, but then the exporting modules have to be updated accordingly.

Module usage
Imported by
Interface:First-order logic, Interface:Basic arithmetic and many others
Exported by
Convenience theorems of propositional logic

Well-formed formulas[edit]

We first introduce the kind of well-formed formulas and a few variables for this kind.

kind (wff)
var (wff p q r s)

Some authors just use the term formula instead of wff, so we define formula to be an alias of wff

kindbind (wff formula)

Logical connectives[edit]

There are five standard logical connectives in the classical propositional calculus, negation,

term (wff (¬ wff))


term (wff ( wff wff))


term (wff ( wff wff))


term (wff ( wff wff))

and, finally, the biconditional,

term (wff ( wff wff))

In addition, one can also consider the constant formulas (or nullary connectives) "the true",

term (wff ())

and "the false",

term (wff ())

Order of operations[edit]

JHilbert requires everything to be parenthesized, and there is no ambiguity about which operations apply to which operands. However, in explanatory text we tend to omit some parentheses for readability, according to the following precedence:

  • ¬
  • →, ↔

For example, ¬ p ∧ q ∨ r → q ∨ r means (((¬ p) ∧ q) ∨ r) → (q ∨ r).

Simple statements[edit]

Here are the statements which do not require any hypotheses.

Constant statements[edit]

The simplest statements are the "true" and the "not false" statement:

stmt (True () () ())
stmt (NotFalse () () (¬ ()))

Negation and implication[edit]

Double negation:

stmt (DoubleNegation () () (p  (¬ (¬ p))))

Implication is reflexive. Sometimes, this is called "Identity" or "Tautology".

stmt (ImplicationReflexivity () () (p  p))

Introduction of an antecedent. Whitehead and Russell call this "Simplification"[1]:

stmt (AntecedentIntroduction () () (p  (q  p)))

Syllogism can be stated in several ways, but this is probably the most familiar:

stmt (ImplicationTransitivity () () (((p  q)  (q  r))  (p  r)))

Syllogism can also applied to formulas with a common antecedent. Other formulas with a common antecedent can be built up using rules such as conjoin, addCommonAntecedent, etc, but we provide this one for convenience:

stmt (SyllogismInConsequent () () ((p  (q  r))  ((p  (r  s))  (p  (q  s)))))

If the consequent of an implication is an implication itself, its antecedent can be distributed over antecedent and consequent of the consequent, and vice versa.

stmt (AntecedentDistribution () () ((p  (q  r))  ((p  q)  (p  r))))

There are three transposition statements:

stmt (Transposition () () ((p  q)  ((¬ q)  (¬ p))))
stmt (TranspositionWithNegatedAntecedent () () (((¬ p)  q)  ((¬ q)  p)))
stmt (TranspositionWithNegatedConsequent () () ((p  (¬ q))  (q  (¬ p))))

Disjunction and conjunction[edit]


stmt (DisjunctionIdempotence () () (p  (p  p)))
stmt (ConjunctionIdempotence () () (p  (p  p)))


stmt (DisjunctionAssociativity () () (((p  q)  r)  (p  (q  r))))
stmt (ConjunctionAssociativity () () (((p  q)  r)  (p  (q  r))))


stmt (DisjunctionCommutativity () () ((p  q)  (q  p)))
stmt (ConjunctionCommutativity () () ((p  q)  (q  p)))


stmt (DisjunctionLeftDistribution () () ((p  (q  r))  ((p  q)  (p  r))))
stmt (DisjunctionRightDistribution () () (((p  q)  r)  ((p  r)  (q  r))))
stmt (ConjunctionLeftDistribution () () ((p  (q  r))  ((p  q)  (p  r))))
stmt (ConjunctionRightDistribution () () (((p  q)  r)  ((p  r)  (q  r))))

De Morgan's laws[edit]

Since De Morgan's laws have many forms, we use the suffix xAy to indicate the form. A law with suffix xAy will have the form (¬ (z B w)) ↔ …, where B is or if A is D or C, respectively. z is p or (¬ p) if z is P or N, respectively. Likewise for w, except that q is used instead of p.

stmt (DeMorganPDP () () ((¬ (p  q))  ((¬ p)  (¬ q))))
stmt (DeMorganPDN () () ((¬ (p  (¬ q)))  ((¬ p)  q)))
stmt (DeMorganNDP () () ((¬ ((¬ p)  q))  (p  (¬ q))))
stmt (DeMorganNDN () () ((¬ ((¬ p)  (¬ q)))  (p  q)))
stmt (DeMorganPCP () () ((¬ (p  q))  ((¬ p)  (¬ q))))
stmt (DeMorganPCN () () ((¬ (p  (¬ q)))  ((¬ p)  q)))
stmt (DeMorganNCP () () ((¬ ((¬ p)  q))  (p  (¬ q))))
stmt (DeMorganNCN () () ((¬ ((¬ p)  (¬ q)))  (p  q)))

Other statements containing negation, implication, disjunction and conjunction[edit]

Although there is no associativity law for implication, we have the following importation/exportation principle due to Guiseppe Peano:

stmt (Transportation () () ((p  (q  r))  ((p  q)  r)))

Two famous implication elimination principles, Modus ponens and modus tollens:

stmt (ModusPonens () () ((p  (p  q))  q))
stmt (ModusTollens () () (((¬ q)  (p  q))  (¬ p)))

Introduction principle for disjunction:

stmt (DisjunctionLeftIntroduction () () (p  (q  p)))
stmt (DisjunctionRightIntroduction () () (p  (p  q)))

Introduction and elimination principles for conjunction:

stmt (ConjunctionLeftIntroduction () () (p  (q  (q  p))))
stmt (ConjunctionRightIntroduction () () (p  (q  (p  q))))
stmt (ConjunctionLeftElimination () () ((p  q)  q))
stmt (ConjunctionRightElimination () () ((p  q)  p))

Case by case elimination:

stmt (CaseElimination () () (((p  q)  ((¬ p)  q))  q))

Composition for disjunction and conjunction:

stmt (DisjunctionComposition () () (((p  r)  (q  r))  ((p  q)  r)))
stmt (ConjunctionComposition () () (((p  q)  (p  r))  (p  (q  r))))

Summation for disjunction. We use the suffixes LL, LR, RL and RR to indicate if the summands were added to the left or the right of antecedent or consequent, respectively.

stmt (DisjunctionSummationLL () () ((p  q)  ((r  p)  (r  q))))
stmt (DisjunctionSummationLR () () ((p  q)  ((r  p)  (q  r))))
stmt (DisjunctionSummationRL () () ((p  q)  ((p  r)  (r  q))))
stmt (DisjunctionSummationRR () () ((p  q)  ((p  r)  (q  r))))
stmt (DisjunctionSummation () () (((p  q)  (r  s))  ((p  r)  (q  s))))

Multiplication for conjunction, with the same suffixes as above.

stmt (ConjunctionMultiplicationLL () () ((p  q)  ((r  p)  (r  q))))
stmt (ConjunctionMultiplicationLR () () ((p  q)  ((r  p)  (q  r))))
stmt (ConjunctionMultiplicationRL () () ((p  q)  ((p  r)  (r  q))))
stmt (ConjunctionMultiplicationRR () () ((p  q)  ((p  r)  (q  r))))
stmt (ConjunctionMultiplication () () (((p  q)  (r  s))  ((p  r)  (q  s))))

Adding a common antecedent to an implication, or adding a common consequent and reversing the direction of the implication:

stmt (CommonAntecedentAddition () () ((q  r)  ((p  q)  (p  r))))
stmt (CommonConsequentAddition () () ((p  q)  ((q  r)  (p  r))))


Equivalence relation[edit]

The biconditional simply creates an equivalence relation among well-formed formulas:

stmt (BiconditionalReflexivity () () (p  p))
stmt (BiconditionalSymmetry () () ((p  q)  (q  p)))
stmt (BiconditionalTransitivity () () (((p  q)  (q  r))  (p  r)))

This equivalence relation creates two equivalence classes, the true and the false formulas:

stmt (Tautology () () ((p  (¬ p))  ()))
stmt (Contradiction () () ((p  (¬ p))  ()))

The left hand side of Tautology is precisely the tertium non datur statement ensuring the existence of at most two truth-values:

stmt (TertiumNonDatur () () (p  (¬ p)))


A biconditional makes a strong statement. Often, we only need a weaker statement. For introductions, see the section on truth function interdependencies.

The naming convention here is that when we think of p ↔ q as consisting of two implications, we call p → q the forward one and q → p the reverse one.

stmt (BiconditionalForwardElimination () () ((p  q)  (q  p)))
stmt (BiconditionalReverseElimination () () ((p  q)  (p  q)))

When we think of a biconditional as two disjunctions, an intuitive naming convention is more elusive, but we currently call (¬ p) ∨ q the left one and p ∨ (¬ q) the right one.

stmt (BiconditionalDisjunctionLeftElimination () () ((p  q)  (p  (¬ q))))
stmt (BiconditionalDisjunctionRightElimination () () ((p  q)  ((¬ p)  q)))

Truth functions[edit]

The logical connectives are functions on the equivalence classes of true and false formulas. That is, if and are formulas such that and are in the same equivalence class for , then an -ary logical connective will send both groups of formulas to the same equivalence class. We express this for our truth functions:

stmt (NegationFunction () () ((p  q)  ((¬ p)  (¬ q))))
stmt (ImplicationFunction () () (((p  q)  (r  s))  ((p  r)  (q  s))))
stmt (DisjunctionFunction () () (((p  q)  (r  s))  ((p  r)  (q  s))))
stmt (ConjunctionFunction () () (((p  q)  (r  s))  ((p  r)  (q  s))))
stmt (BiconditionalFunction () () (((p  q)  (r  s))  ((p  r)  (q  s))))

Note that only negation has as its leading connective because it is the only truth function which is injective

Truth function interdependencies[edit]

The truth functions are not always independent of each other. We have already seen that in De Morgan's laws. Here are the remaining important interdependencies: Biconditional as bidirectional implication:

stmt (BiconditionalImplication () () ((p  q)  ((p  q)  (q  p))))

Biconditional as disjunction of the two equivalence classes:

stmt (BiconditionalDisjunction () () ((p  q)  ((p  q)  ((¬ p)  (¬ q)))))

Biconditional as conjunction:

stmt (BiconditionalConjunction () () ((p  q)  (((¬ p)  q)  (p  (¬ q)))))

Implication as disjunction:

stmt (ImplicationDisjunction () () ((p  q)  ((¬ p)  q)))

Disjunction as implication:

stmt (DisjunctionImplication () () ((p  q)  ((¬ p)  q)))

Negation as implication:

stmt (NegationImplication () () ((¬ p)  (p  ())))


Transposition applies for the biconditional as well as for the implication, although commutativity means that some of the theorems can look different while still covering the same territory. The NegationFunction theorem covers the case in which both or neither side is negated, and the following covers the case in which one side is negated:

stmt (BiconditionalTranspositionWithNegatedRight () () ((p  (¬ q))  (q  (¬ p))))

Antecedent distribution[edit]

Here is a version of AntecedentDistribution with one of the implications replaced by a biconditional.

stmt (ImplicationDistributionOverBiconditional () () ((p  (q  r))  ((p  q)  (p  r))))

Biconditional and conjunction[edit]

A true conjunct does not affect the truth of a proposition.

stmt (BiconditionalConjunct () () (q  (p  (p  q))))

Two true propositions are equivalent.

stmt (TruthBiconditional () () ((p  q)  (p  q)))


Each propositional calculus needs at least one rule of detachment (modus ponens appears to be the most common). However, it will be convenient to have certain toolbox of rules implementing often used statements.

Negation and implication:

stmt (introduceDoubleNegation () (p) (¬ (¬ p)))
stmt (eliminateDoubleNegation () ((¬ (¬ p))) p)
stmt (introduceAntecedent () (p) (q  p))
stmt (applySyllogism () ((p  q) (q  r)) (p  r))
stmt (applySyllogismInConsequent () ((p  (q  r)) (p  (r  s))) (p  (q  s)))
stmt (distributeAntecedent () ((p  (q  r))) ((p  q)  (p  r)))
stmt (collectAntecedent () (((p  q)  (p  r))) (p  (q  r)))
stmt (eliminateTransposition () (((¬ q)  (¬ p))) (p  q))
stmt (introduceTransposition () ((p  q)) ((¬ q)  (¬ p)))
stmt (transposeWithNegatedAntecedent () (((¬ p)  q)) ((¬ q)  p))
stmt (transposeWithNegatedConsequent () ((p  (¬ q))) (q  (¬ p)))

Disjunction and conjunction:

stmt (cloneAsDisjunction () (p) (p  p))
stmt (conflateDisjunction () ((p  p)) p)
stmt (cloneAsConjunction () (p) (p  p))
stmt (conflateConjunction () ((p  p)) p)
stmt (groupDisjunctionLeft () ((p  (q  r))) ((p  q)  r))
stmt (groupDisjunctionRight () (((p  q)  r)) (p  (q  r)))
stmt (groupConjunctionLeft () ((p  (q  r))) ((p  q)  r))
stmt (groupConjunctionRight () (((p  q)  r)) (p  (q  r)))
stmt (swapDisjunction () ((p  q)) (q  p))
stmt (swapConjunction () ((p  q)) (q  p))
stmt (distributeLeftDisjunction () ((p  (q  r))) ((p  q)  (p  r)))
stmt (collectLeftDisjunction () (((p  q)  (p  r))) (p  (q  r)))
stmt (distributeRightDisjunction () (((p  q)  r)) ((p  r)  (q  r)))
stmt (collectRightDisjunction () (((p  r)  (q  r))) ((p  q)  r))
stmt (distributeLeftConjunction () ((p  (q  r))) ((p  q)  (p  r)))
stmt (collectLeftConjunction () (((p  q)  (p  r))) (p  (q  r)))
stmt (distributeRightConjunction () (((p  q)  r)) ((p  r)  (q  r)))
stmt (collectRightConjunction () (((p  r)  (q  r))) ((p  q)  r))

De Morgan's laws:

stmt (distributeNegationPDP () ((¬ (p  q))) ((¬ p)  (¬ q)))
stmt (distributeNegationPDN () ((¬ (p  (¬ q)))) ((¬ p)  q))
stmt (distributeNegationNDP () ((¬ ((¬ p)  q))) (p  (¬ q)))
stmt (distributeNegationNDN () ((¬ ((¬ p)  (¬ q)))) (p  q))
stmt (distributeNegationPCP () ((¬ (p  q))) ((¬ p)  (¬ q)))
stmt (distributeNegationPCN () ((¬ (p  (¬ q)))) ((¬ p)  q))
stmt (distributeNegationNCP () ((¬ ((¬ p)  q))) (p  (¬ q)))
stmt (distributeNegationNCN () ((¬ ((¬ p)  (¬ q)))) (p  q))
stmt (collectNegationPDP () ((p  q)) (¬ ((¬ p)  (¬ q))))
stmt (collectNegationPDN () ((p  (¬ q))) (¬ ((¬ p)  q)))
stmt (collectNegationNDP () (((¬ p)  q)) (¬ (p  (¬ q))))
stmt (collectNegationNDN () (((¬ p)  (¬ q))) (¬ (p  q)))
stmt (collectNegationPCP () ((p  q)) (¬ ((¬ p)  (¬ q))))
stmt (collectNegationPCN () ((p  (¬ q))) (¬ ((¬ p)  q)))
stmt (collectNegationNCP () (((¬ p)  q)) (¬ (p  (¬ q))))
stmt (collectNegationNCN () (((¬ p)  (¬ q))) (¬ (p  q)))

Other rules containing negation, implication, disjunction and conjunction:

stmt (import () ((p  (q  r))) ((p  q)  r))
stmt (export () (((p  q)  r)) (p  (q  r)))
stmt (applyModusPonens () (p (p  q)) q)
stmt (applyModusTollens () ((¬ q) (p  q)) (¬ p))
stmt (introduceLeftDisjunction () (p) (q  p))
stmt (introduceRightDisjunction () (p) (p  q))
stmt (introduceConjunction () (p q) (p  q))
stmt (eliminateLeftConjunct () ((p  q)) q)
stmt (eliminateRightConjunct () ((p  q)) p)
stmt (eliminateCases () ((p  q) ((¬ p)  q)) q)
stmt (composeDisjunction () ((p  r) (q  r)) ((p  q)  r))
stmt (extractLeftDisjunction () (((p  q)  r)) (p  r))
stmt (extractRightDisjunction () (((p  q)  r)) (q  r))
stmt (composeConjunction () ((p  q) (p  r)) (p  (q  r)))
stmt (extractLeftConjunction () ((p  (q  r))) (p  q))
stmt (extractRightConjunction () ((p  (q  r))) (p  r))
stmt (disjoinLL () ((p  q)) ((r  p)  (r  q)))
stmt (disjoinLR () ((p  q)) ((r  p)  (q  r)))
stmt (disjoinRL () ((p  q)) ((p  r)  (r  q)))
stmt (disjoinRR () ((p  q)) ((p  r)  (q  r)))
stmt (disjoin () ((p  q) (r  s)) ((p  r)  (q  s)))
stmt (conjoinLL () ((p  q)) ((r  p)  (r  q)))
stmt (conjoinLR () ((p  q)) ((r  p)  (q  r)))
stmt (conjoinRL () ((p  q)) ((p  r)  (r  q)))
stmt (conjoinRR () ((p  q)) ((p  r)  (q  r)))
stmt (conjoin () ((p  q) (r  s)) ((p  r)  (q  s)))
stmt (addCommonAntecedent () ((q  r)) ((p  q)  (p  r)))
stmt (addCommonConsequent () ((p  q)) ((q  r)  (p  r)))


stmt (swapBiconditional () ((p  q)) (q  p))
stmt (applyBiconditionalTransitivity () ((p  q) (q  r)) (p  r))
stmt (eliminateBiconditionalForward () ((p  q)) (q  p))
stmt (eliminateBiconditionalReverse () ((p  q)) (p  q))
stmt (eliminateLeftBiconditionalDisjunction () ((p  q)) (p  (¬ q)))
stmt (eliminateRightBiconditionalDisjunction () ((p  q)) ((¬ p)  q))
stmt (addNegation () ((p  q)) ((¬ p)  (¬ q)))
stmt (removeNegation () (((¬ p)  (¬ q))) (p  q))
stmt (buildImplication () ((p  q) (r  s)) ((p  r)  (q  s)))
stmt (buildDisjunction () ((p  q) (r  s)) ((p  r)  (q  s)))
stmt (buildConjunction () ((p  q) (r  s)) ((p  r)  (q  s)))
stmt (buildBiconditional () ((p  q) (r  s)) ((p  r)  (q  s)))
stmt (convertFromBiconditionalToImplications () ((p  q)) ((p  q)  (q  p)))
stmt (convertToBiconditionalFromImplications () (((p  q)  (q  p))) (p  q))
stmt (introduceBiconditionalFromImplications () ((p  q) (q  p)) (p  q))
stmt (convertFromBiconditionalToDisjunction () ((p  q)) ((p  q)  ((¬ p)  (¬ q))))
stmt (convertToBiconditionalFromDisjunction () (((p  q)  ((¬ p)  (¬ q)))) (p  q))
stmt (convertFromBiconditionalToConjunction () ((p  q)) (((¬ p)  q)  (p  (¬ q))))
stmt (convertToBiconditionalFromConjunction () ((((¬ p)  q)  (p  (¬ q)))) (p  q))
stmt (introduceBiconditionalFromDisjunctions () (((¬ p)  q) (p  (¬ q))) (p  q))
stmt (convertFromImplicationToDisjunction () ((p  q)) ((¬ p)  q))
stmt (convertToImplicationFromDisjunction () (((¬ p)  q)) (p  q))
stmt (convertFromDisjunctionToImplication () ((p  q)) ((¬ p)  q))
stmt (convertToDisjunctionFromImplication () (((¬ p)  q)) (p  q))
stmt (convertFromNegationToImplication () ((¬ p)) (p  ()))
stmt (convertToNegationFromImplication () ((p  ())) (¬ p))
stmt (transposeBiconditionalWithNegatedRight () ((p  (¬ q))) (q  (¬ p)))
stmt (distributeImplicationOverBiconditional () ((p  (q  r))) ((p  q)  (p  r)))

Convenience theorems and rules[edit]

Additional builders[edit]

var (formula antecedent consequent common p0 q0 p1 q1)

stmt (DisjunctionBuilderLL () () ((p  q)  ((common  p)  (common  q))))
stmt (buildDisjunctionLL () ((p  q)) ((common  p)  (common  q)))
stmt (DisjunctionBuilderRR () () ((p  q)  ((p  common)  (q  common))))
stmt (buildDisjunctionRR () ((p  q)) ((p  common)  (q  common)))

stmt (buildConjunctionLL () ((p  q)) ((r  p)  (r  q)))
stmt (buildConjunctionRR () ((p  q)) ((p  r)  (q  r)))
stmt (BiconditionalBuilderRR () () ((p  q)  ((p  common)  (q  common))))
stmt (buildBiconditionalLL () ((p  q)) ((common  p)  (common  q)))

stmt (ImplicationBuilderRR () () ((p  q)  ((p  common)  (q  common))))
stmt (ImplicationBuilderConsequent () () ((p  q)  ((p  common)  (q  common))))
stmt (buildImplicationConsequent () ((p  q)) ((p  common)  (q  common)))
stmt (buildImplicationAntecedent () ((p  q)) ((common  p)  (common  q)))

stmt (addNegationInConsequent () ((antecedent  (p  q))) (antecedent  ((¬ p)  (¬ q))))
stmt (buildConjunctionRRInConsequent ()
  ((antecedent  (p  q)))
  (antecedent  ((p  common)  (q  common))))
stmt (buildConjunctionLLInConsequent ()
  ((antecedent  (p  q)))
  (antecedent  ((common  p)  (common  q))))
stmt (buildDisjunctionRRInConsequent () ((antecedent  (p  q))) (antecedent  ((p  common)  (q  common))))
stmt (buildDisjunctionLLInConsequent () ((antecedent  (p  q))) (antecedent  ((common  p)  (common  q))))
stmt (buildConjunctionInConsequent ()
  ((antecedent  (p0  q0))
   (antecedent  (p1  q1)))
  (antecedent  ((p0  p1)  (q0  q1))))
stmt (buildDisjunctionInConsequent ()
  ((antecedent  (p0  q0))
   (antecedent  (p1  q1)))
  (antecedent  ((p0  p1)  (q0  q1))))

stmt (buildCommonAntecedentInConsequent ()
  ((antecedent  (p  q)))
  (antecedent  ((common  p)  (common  q))))
stmt (buildCommonConsequentInConsequent ()
  ((antecedent  (p  q)))
  (antecedent  ((p  common)  (q  common))))
stmt (buildImplicationInConsequent ()
  ((antecedent  (p0  q0))
   (antecedent  (p1  q1)))
  (antecedent  ((p0  p1)  (q0  q1))))
stmt (buildBiconditionalInConsequent ()
  ((antecedent  (p0  q0))
   (antecedent  (p1  q1)))
  (antecedent  ((p0  p1)  (q0  q1))))
stmt (buildBiconditionalLLInConsequent () ((antecedent  (p  q))) (antecedent  ((common  p)  (common  q))))
stmt (buildBiconditionalRRInConsequent () ((antecedent  (p  q))) (antecedent  ((p  common)  (q  common))))

Various theorems in the consequent[edit]

stmt (introduceBiconditionalFromImplicationsInConsequent () ((antecedent  (p  q)) (antecedent  (q  p))) (antecedent  (p  q)))
stmt (eliminateBiconditionalReverseInConsequent () ((antecedent  (p  q))) (antecedent  (p  q)))
stmt (eliminateBiconditionalForwardInConsequent () ((antecedent  (p  q))) (antecedent  (q  p)))
stmt (applyModusPonensInConsequent () ((antecedent  p) (antecedent  (p  q))) (antecedent  q))
stmt (applyBiconditionalTransitivityInConsequent ()
  ((antecedent  (p  q))
   (antecedent  (q  r)))
  (antecedent  (p  r)))
stmt (swapBiconditionalInConsequent () ((antecedent  (p  q))) (antecedent  (q  p)))

stmt (introduceAntecedentInConsequent () ((antecedent  p)) (antecedent  (q  p)))
stmt (importInConsequent ()
  ((antecedent  (p  (q  r))))
  (antecedent  ((p  q)  r)))
stmt (exportInConsequent ()
  ((antecedent  ((p  q)  r)))
  (antecedent  (p  (q  r))) )

stmt (eliminateLeftConjunctInConsequent () ((antecedent  (p  q))) (antecedent  q))
stmt (eliminateRightConjunctInConsequent () ((antecedent  (p  q))) (antecedent  p))

stmt (introduceTranspositionInConsequent ()
  ((antecedent  (p  q)))
  (antecedent  ((¬ q)  (¬ p))))
stmt (eliminateTranspositionInConsequent ()
  ((antecedent  ((¬ q)  (¬ p))))
  (antecedent  (p  q)))

Theorems partly in the consequent[edit]

We can have a theorem not in the consequent (for example, introduceConjunction derives p ∧ q from hypotheses p and q). We can have a theorem entirely in the consequent–that is, all hypotheses have a common antecedent (for example, composeConjunction derives antecedent → p ∧ q from antecedent → p and antecedent → q). In this section we have some theorems in which some, but not all, hypotheses have a common antecedent which also figures in the conclusion.[2]

stmt (introduceLeftConjunctToConsequent () ((antecedent  p) q) (antecedent  (q  p)))
stmt (introduceRightConjunctToConsequent () ((antecedent  p) q) (antecedent  (p  q)))

Theorems in the antecedent[edit]

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.

stmt (importInAntecedent ()
  (((p  (q  r))  consequent))
  (((p  q)  r)  consequent))
stmt (exportInAntecedent ()
  ((((p  q)  r)  consequent))
  ((p  (q  r))  consequent))


These are analogues to modus ponens, but where some other portion of the formula, other than a single antecedent, is detached.

stmt (detach1of2 () (p ((p  q)  r)) (q  r))
stmt (detach2of2 () (q ((p  q)  r)) (p  r))

stmt (detach1of3 () (p (((p  q)  r)  consequent)) ((q  r)  consequent))
stmt (detach2of3 () (q (((p  q)  r)  consequent)) ((p  r)  consequent))
# Invoke detach2of2 to detach the third of three antecedents

stmt (detach1of4 () (p ((((p  q)  r)  s)  consequent)) (((q  r)  s)  consequent))
# Invoke detach2of3 to detach the third of four antecedents
# Invoke detach2of2 to detach the fourth of four antecedents

stmt (detachImplicationBiconditional () (q (p  (q  r))) (p  r))
stmt (detachImplicationBiconditionalRight () (r (p  (q  r))) (p  q))
stmt (detachImplicationImplication () (p (antecedent  (p  q))) (antecedent  q))

Negated detachment[edit]

These are variants of modus tollens where we detach a portion of a formula which is more complicated than just a single implication.

stmt (negatedDetachImplicationBiconditionalRight () ((¬ r) (p  (q  r))) (p  (¬ q)))
stmt (negatedDetachImplicationBiconditional () ((¬ q) (p  (q  r))) (p  (¬ r)))
stmt (negatedDetachImplicationImplication () ((¬ r) (p  (q  r))) (p  (¬ q)))

Commutation of antecedents[edit]

This result is a consequence of import/export and conjunction commutativity.

stmt (applyComm () ((p  (q  r))) (q  (p  r)))


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

stmt (transformAntecedent () ((p  q) (p  r)) (r  q))
stmt (transformImplicationImplicationConsequent () ((antecedent  (p  q)) (q  r)) (antecedent  (p  r)))
stmt (transformImplicationImplicationAntecedent () ((antecedent  (p  q)) (p  r)) (antecedent  (r  q)))
stmt (transformImplicationBiconditionalLeft () ((antecedent  (p  q)) (p  r)) (antecedent  (r  q)))
stmt (transformImplicationBiconditionalRight () ((antecedent  (p  q)) (q  r)) (antecedent  (p  r)))
stmt (transformImplicationDisjunctionLeft () ((antecedent  (p  q)) (p  r)) (antecedent  (r  q)))
stmt (transformDisjunctionRight () ((p  q) (q  r)) (p  r))

Additional relationships between connectives[edit]

stmt (ConjunctionImplication () () ((p  q)  (¬ (p  (¬ q)))))
stmt (ImplicationConjunction () () ((p  q)  (¬ (p  (¬ q)))))

stmt (NegationBiconditional () () ((¬ p)  (p  ())))

Rules for associativity[edit]

Zeichen 123 - Baustelle, StVO 1992.svg This page or section needs cleanup. You can help wikiproofs by renaming these to groupConjunction* or renaming groupConjunctionRight to associateConjunctionRight and likewise for the other group* ones. Talk page discussion would be a good way to figure out which rename is better. See Help:Contents if you haven't yet figured out how to edit and write proofs, or ask at WP:TEA if you have any questions.

stmt (associateConjunctionRightInConsequent () ((antecedent  ((p  q)  r)))
  (antecedent  (p  (q  r))))
stmt (associateConjunctionLeftInConsequent () ((antecedent  (p  (q  r))))
  (antecedent  ((p  q)  r)))

Combinations of commutativity and associativity[edit]

Commutativity and associativity might be combined in any number of ways, but a few patterns turn out to be common.

stmt (Disjunction4 () () (((p  q)  (r  s))  ((p  r)  (q  s))))
stmt (swap23ofDisjunction4 () (((p  q)  (r  s))) ((p  r)  (q  s)))
stmt (swap23ofDisjunction3 () (((p  q)  r)) ((p  r)  q))
stmt (swap12ofDisjunction3 () (((p  q)  r)) ((q  p)  r))

stmt (Conjunction4 () () (((p  q)  (r  s))  ((p  r)  (q  s))))

Proof by contradiction[edit]

Although Contradiction and similar theorems provide some tools for proof by contradiction, here are some rules to make it easier.

stmt (noteContradiction () ((p  q) (p  (¬ q))) (¬ p))
stmt (deduceNegationFromContradiction () ((p  (¬ p))) (¬ p))
stmt (deduceFromNegatedContradiction () (((¬ p)  p)) p)


  1. A. Whitehead, B. Russell, Principia Mathematica, Cambridge University Press, 1910.
  2. introduceLeftConjunctToConsequent is jctil in metamath, accessed December 2010. introduceRightConjunctToConsequent is jctir

Interface module parsed successfully