# [[From intuitionistic to classical propositional logic]] # }} # # == Well-formed formulas == # # We first introduce the kind of [[w:well-formed formulas|well-formed formulas]] and a few variables for this kind. kind (formula) tvar (formula p q r s) # # == Logical connectives == # # There are five standard [[w:logical connective|logical connective]]s in the classical propositional calculus, [[w:negation|negation]], term (formula (¬ p)) # [[w:material conditional|implication]], term (formula (→ p q)) # [[w:logical disjunction|disjunction]], term (formula (∨ p q)) # [[w:logical conjunction|conjunction]], term (formula (∧ p q)) # and, finally, the [[w:logical biconditional|biconditional]], term (formula (↔ p q)) # In addition, one can also consider the constant formulas (or [[w:nullary#Nullary|nullary]] connectives) "the true", term (formula (⊤)) # and "the false", term (formula (⊥)) # # == Simple statements == # # Here are the statements which do not require any hypotheses. # # === Constant statements === # # The simplest statements are the "true" and the "not false" statement: stmt (True () () (⊤)) stmt (NotFalse () () (¬ (⊥))) # # === Negation and implication === # # [[w:double negative elimination|Double negation]]: stmt (DoubleNegation () () (↔ p (¬ (¬ p)))) # Implication is [[w:reflexive relation|reflexive]]. Sometimes, this is called "Identity" or "Tautology". stmt (ImplicationReflexivity () () (→ p p)) # Introduction of an [[w:antecedent (logic)|antecedent]]. Whitehead and Russell call this "Simplification"{{sc|A. Whitehead, B. Russell}}, Principia Mathematica, ''Cambridge University Press'', 1910.: stmt (AntecedentIntroduction () () (→ p (→ q p))) # [[w:Syllogism|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 [[w:consequent|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 [[w:Transposition_(logic)|transposition]] statements:
stmt (Transposition () () (↔ (→ p q) (→ (¬ q) (¬ p))))
stmt (TranspositionWithNegatedAntecedent () () (↔ (→ (¬ p) q) (→ (¬ q) p)))
stmt (TranspositionWithNegatedConsequent () () (↔ (→ p (¬ q)) (→ q (¬ p))))
#
# === Disjunction and conjunction ===
#
# [[w:Idempotence|Idempotence]]:
stmt (DisjunctionIdempotence () () (↔ p (∨ p p)))
stmt (ConjunctionIdempotence () () (↔ p (∧ p p)))
#
# [[w:Associativity|Associativity]]:
stmt (DisjunctionAssociativity () () (↔ (∨ (∨ p q) r) (∨ p (∨ q r))))
stmt (ConjunctionAssociativity () () (↔ (∧ (∧ p q) r) (∧ p (∧ q r))))
#
# [[w:Commutativity|Commutativity]]:
stmt (DisjunctionCommutativity () () (↔ (∨ p q) (∨ q p)))
stmt (ConjunctionCommutativity () () (↔ (∧ p q) (∧ q p)))
#
# [[w:Distributivity|Distributivity]]:
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 ===
#
# Since [[w:De Morgan's laws|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 ===
#
# Although there is no associativity law for implication, we have the following importation/exportation principle due to [[w:Guiseppe Peano|Guiseppe Peano]]:
stmt (Transportation () () (↔ (→ p (→ q r)) (→ (∧ p q) r)))
# Two famous implication elimination principles, [[w:Modus ponens|Modus ponens]] and [[w:modus tollens|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))))
#
# === Biconditional ===
#
# ==== Equivalence relation ====
#
# The biconditional simply creates an [[w:equivalence relation|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 [[w:equivalence class|equivalence class]]es, the true and the false formulas:
stmt (Tautology () () (↔ (∨ p (¬ p)) (⊤)))
stmt (Contradiction () () (↔ (∧ p (¬ p)) (⊥)))
# The left hand side of ''Tautology'' is precisely the [[w:tertium non datur|tertium non datur]] statement ensuring the existence of at most two truth-values:
stmt (TertiumNonDatur () () (∨ p (¬ p)))
#
# ==== Weakenings ====
#
# A biconditional makes a strong statement. Often, we only need a weaker statement. For introductions, see the section on [[#Truth function interdependencies|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 ====
#
# The logical connectives are functions on the equivalence classes of true and false formulas. That is, if $p\_1,\backslash ldots,p\_n$ and $q\_1,\backslash ldots,q\_n$ are formulas such that $p\_i$ and $q\_i$ are in the same equivalence class for $i=1,\backslash ldots,n$, then an $n$-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 [[w:injective|injective]]
#
# ==== Truth function interdependencies ====
#
# 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 ====
# 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 ====
# 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 ====
# 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)))
#
# == Rules ==
#
# 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)))
# Biconditional:
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)))
#
# == References ==
#
#