Convenience theorems of intuitionistic propositional logic

From Wikiproofs
Jump to: navigation, search
Convenience theorems of intuitionistic propositional logic
This page proves those statments of Interface:Intuitionistic propositional logic which aren't in Interface:Basic intuitionistic propositional logic. This includes chiefly additional builders (which aren't necessary in most textbook treatments as they take substitution for granted), additional variants on modus ponens and related theorems, and the like. As it turns out the majority of convenience theorems of this sort are the same between classical and intuitionistic logic.
Used interfaces
Imports
Interface:Basic intuitionistic propositional logic
Exports
Interface:Intuitionistic propositional logic

Here we import Interface:Basic intuitionistic propositional logic (where our classical counterpart imports 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.

var (formula p q r s antecedent common)

Detachment[edit]

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

Multiple antecedents[edit]

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.

thm (detach1of2 () ((H p) (HIMP ((p  q)  r))) (q  r) (
        H
        HIMP export
        applyModusPonens
))

thm (detach2of2 () ((H q) (HIMP ((p  q)  r))) (p  r) (
        H

        q p ConjunctionCommutativity eliminateBiconditionalReverse
        HIMP
        applySyllogism

        export
        applyModusPonens
))

var (formula consequent)
thm (detach1of3 () ((H p) (HIMP (((p  q)  r)  consequent))) ((q  r)  consequent) (
        H

        HIMP
        export
        export

        applyModusPonens

        import
))

thm (detach2of3 () ((H q) (HIMP (((p  q)  r)  consequent))) ((p  r)  consequent) (
        H

        q p ConjunctionCommutativity eliminateBiconditionalReverse
        HIMP
        export
        applySyllogism

        export
        applyModusPonens

        import
))

thm (detach1of4 () ((H p) (HIMP ((((p  q)  r)  s)  consequent))) (((q  r)  s)  consequent) (
        H

        HIMP
        export
        export
        export

        applyModusPonens

        import
        import
))

Nested formulas[edit]

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.

thm (applyComm () ((H (p  (q  r)))) (q  (p  r)) (
        H
        import

        q p ConjunctionCommutativity eliminateBiconditionalReverse
        r addCommonConsequent

        applyModusPonens
        export
))

thm (detachImplicationImplication () 
  ((H p) (HIMP (antecedent  (p  q))))
  (antecedent  q) (
        H
        HIMP
        applyComm
        applyModusPonens
))

thm (detachImplicationBiconditional () 
  ((H q) 
   (HIMP (p  (q  r))))
  (p  r) (
        H

        HIMP
        q r BiconditionalReverseElimination
        applySyllogism
        import

        detach2of2
))

thm (detachImplicationBiconditionalRight () 
  ((H r) 
   (HIMP (p  (q  r))))
  (p  q) (
        H

        HIMP
        q r BiconditionalSymmetry eliminateBiconditionalReverse
        applySyllogism

        detachImplicationBiconditional
))

Negated detachment[edit]

This variant of modus tollens detaches the right hand side of a biconditional, which is a consequent.[1]

thm (negatedDetachImplicationBiconditionalRight () 
  ((H (¬ r)) 
   (HIMP (p  (q  r))))
  (p  (¬ q)) (
        H

        HIMP
        q r NegationBuilder
        applySyllogism

        detachImplicationBiconditionalRight
))

Here's the same thing for the left side of the biconditional.

thm (negatedDetachImplicationBiconditional () 
  ((H (¬ q)) 
   (HIMP (p  (q  r))))
  (p  (¬ r)) (
        H

        HIMP
        q r NegationBuilder
        applySyllogism

        detachImplicationBiconditional
))

Here's one for two implications.

thm (negatedDetachImplicationImplication () 
  ((H (¬ r)) 
   (HIMP (p  (q  r))))
  (p  (¬ q)) (
        H

        HIMP
        q r TranspositionIntroduction
        applySyllogism

        detachImplicationImplication
))

Transforming parts of formula[edit]

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

thm (transformAntecedent () ((HIMP (p  q)) (HEQ (p  r))) (r  q) (
        HEQ eliminateBiconditionalForward
        HIMP
        applySyllogism
))

thm (transformImplicationImplicationConsequent () ((HIMP (antecedent  (p  q))) (HEQ (q  r))) (antecedent  (p  r)) (
        HIMP

        HEQ eliminateBiconditionalReverse
        p addCommonAntecedent
        antecedent addCommonAntecedent

        applyModusPonens
))

thm (transformImplicationImplicationAntecedent ()
  ((HIMP (antecedent  (p  q))) (HEQ (p  r)))
  (antecedent  (r  q)) (
        HEQ eliminateBiconditionalForward
        antecedent introduceAntecedent

        HIMP

        applySyllogismInConsequent
))

thm (transformImplicationBiconditionalLeft () ((HIMP (antecedent  (p  q))) (HEQ (p  r))) (antecedent  (r  q)) (
        HEQ
        swapBiconditional
        antecedent introduceAntecedent

        HIMP

        composeConjunction
        
        r p q BiconditionalTransitivity

        applySyllogism
))

thm (transformImplicationBiconditionalRight () ((HIMP (antecedent  (p  q))) (HEQ (q  r))) (antecedent  (p  r)) (
        HIMP

        HEQ
        antecedent introduceAntecedent
        composeConjunction
        
        p q r BiconditionalTransitivity

        applySyllogism
))

thm (transformDisjunctionRight () ((H (p  q)) (HEQ (q  r))) (p  r) (
        H

        HEQ
        eliminateBiconditionalReverse
        p disjoinLL

        applyModusPonens
))

More relationships between connectives[edit]

Conjunction and implication[edit]

We omit the ConjunctionImplication theorem from Convenience theorems of propositional logic, which is p ∧ q ↔ ¬ (p → ¬ q), and ImplicationConjunction, which is (p → q) ↔ ¬ (p ∧ ¬ q).

Negation and biconditional[edit]

We have already proved that ¬ p ↔ (p → ⊥). As in classical logic, we can also show ¬ p ↔ (p ↔ ⊥), but the proof in Convenience theorems of propositional logic doesn't work. Zeichen 123 - Baustelle, StVO 1992.svg This page or section needs cleanup. You can help wikiproofs by finishing the proof here, assuming that it holds in intuitionistic logic. 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.Zeichen 123 - Baustelle, StVO 1992.svg This page or section needs cleanup. You can help wikiproofs by renaming Explosion from Interface:Axioms of intuitionistic propositional logic, perhaps to ExplosionExported or ExplosionAxiom or something, proving Explosion (called ExplosionImported below just to be clear) as p ∧ ¬ p → q, and then exporting it from Intuitionistic propositional logic. 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.


#thm (FalsityExplosion () () ((¬ p) → ((⊥) → p)) (

#        p Contradiction

#        eliminateBiconditionalForward

That gives us ⊥ → p ∧ ¬ p. The consequent of that in turn implies anything, in this case p.

#        p p ExplosionImported

#        applySyllogism

#        (¬ p) introduceAntecedent

#))

Additional builders[edit]

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.

thm (DisjunctionBuilderLL () () ((p  q)  ((r  p)  (r  q))) (
        r BiconditionalReflexivity
        r r p q DisjunctionFunction export
        applyModusPonens
))

thm (buildDisjunctionLL () ((H (p  q)))
  ((r  p)  (r  q)) (
        H
        p q r DisjunctionBuilderLL
        applyModusPonens
))

thm (DisjunctionBuilderRR () () ((p  q)  ((p  common)  (q  common))) (
        common BiconditionalReflexivity
        p q common common DisjunctionFunction
        detach2of2
))

thm (buildDisjunctionRR () ((H (p  q)))
  ((p  common)  (q  common)) (
        H
        p q common DisjunctionBuilderRR
        applyModusPonens
))

thm (buildConjunctionLL () ((H (p  q))) ((r  p)  (r  q)) (
        r BiconditionalReflexivity
        H
        buildConjunction
))

thm (buildConjunctionRR () ((H (p  q))) ((p  r)  (q  r)) (
        H
        r BiconditionalReflexivity
        buildConjunction
))

thm (BiconditionalBuilderRR () () ((p  q)  ((p  common)  (q  common))) (

We first derive (p ↔ q) → ((p ↔ q) ∧ (common ↔ common)):

        common BiconditionalReflexivity
        (common  common) (p  q) ConjunctionLeftIntroduction
        applyModusPonens

Then we just need to apply BiconditionalFunction:

        p q common common BiconditionalFunction
        applySyllogism
))

thm (buildBiconditionalLL () ((H (p  q))) ((common  p)  (common  q)) (
        common BiconditionalReflexivity
        H
        buildBiconditional
))

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

thm (ImplicationBuilderConsequent () () ((p  q)  ((p  common)  (q  common))) (
        common BiconditionalReflexivity
        (common  common) (p  q) ConjunctionLeftIntroduction
        applyModusPonens

        p q common common ImplicationFunction
        applySyllogism
))

thm (ImplicationBuilderRR () () ((p  q)  ((p  common)  (q  common))) (
        p q common ImplicationBuilderConsequent
))

thm (buildImplicationConsequent () ((H (p  q))) ((p  common)  (q  common)) (
        H
        common BiconditionalReflexivity
        buildImplication
))

thm (buildImplicationAntecedent () ((H (p  q))) ((common  p)  (common  q)) (
        common BiconditionalReflexivity
        H
        buildImplication
))

Building in the consequent[edit]

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.

thm (addNegationInConsequent () ((H (antecedent  (p  q)))) (antecedent  ((¬ p)  (¬ q))) (
        H
        p q NegationBuilder
        applySyllogism
))

thm (buildConjunctionRRInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  ((p  common)  (q  common))) (
        H
        common BiconditionalReflexivity
        p q common common ConjunctionFunction detach2of2
        applySyllogism
))

thm (buildConjunctionLLInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  ((common  p)  (common  q))) (
        H
        common BiconditionalReflexivity
        common common p q ConjunctionFunction detach1of2
        applySyllogism
))

thm (buildDisjunctionRRInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  ((p  common)  (q  common))) (
        H
        common BiconditionalReflexivity
        p q common common DisjunctionFunction detach2of2
        applySyllogism
))

thm (buildDisjunctionLLInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  ((common  p)  (common  q))) (
        H
        common BiconditionalReflexivity
        common common p q DisjunctionFunction detach1of2
        applySyllogism
))

var (formula p0 q0 p1 q1)
thm (buildConjunctionInConsequent ()
  ((H0 (antecedent  (p0  q0)))
   (H1 (antecedent  (p1  q1))))
  (antecedent  ((p0  p1)  (q0  q1))) (
        H0 H1 composeConjunction
        p0 q0 p1 q1 ConjunctionFunction
        applySyllogism
))

thm (buildDisjunctionInConsequent ()
  ((H0 (antecedent  (p0  q0)))
   (H1 (antecedent  (p1  q1))))
  (antecedent  ((p0  p1)  (q0  q1))) (
        H0
        H1
        composeConjunction
        p0 q0 p1 q1 DisjunctionFunction
        applySyllogism
))

thm (buildCommonConsequentInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  ((p  common)  (q  common))) (
        H
        common BiconditionalReflexivity
        p q common common ImplicationFunction detach2of2
        applySyllogism
))

thm (buildCommonAntecedentInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  ((common  p)  (common  q))) (
        H
        common BiconditionalReflexivity
        common common p q ImplicationFunction detach1of2
        applySyllogism
))

thm (buildImplicationInConsequent ()
  ((H0 (antecedent  (p0  q0)))
   (H1 (antecedent  (p1  q1))))
  (antecedent  ((p0  p1)  (q0  q1))) (
        H0 H1 composeConjunction
        p0 q0 p1 q1 ImplicationFunction
        applySyllogism
))

thm (buildBiconditionalInConsequent ()
  ((H0 (antecedent  (p0  q0)))
   (H1 (antecedent  (p1  q1))))
  (antecedent  ((p0  p1)  (q0  q1))) (
        H0 H1 composeConjunction
        p0 q0 p1 q1 BiconditionalFunction
        applySyllogism
))

thm (buildBiconditionalLLInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  ((common  p)  (common  q))) (
        H
        common BiconditionalReflexivity
        common common p q BiconditionalFunction detach1of2
        applySyllogism
))

thm (buildBiconditionalRRInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  ((p  common)  (q  common))) (
        H
        common BiconditionalReflexivity
        p q common common BiconditionalFunction detach2of2
        applySyllogism
))

Additional transformations[edit]

thm (transformImplicationDisjunctionLeft () ((HIMP (antecedent  (p  q))) (HEQ (p  r))) (antecedent  (r  q)) (
        HIMP

        antecedent BiconditionalReflexivity
        HEQ
        q buildDisjunctionRR
        buildImplication

        eliminateBiconditionalReverse

        applyModusPonens
))

Additional theorems in the consequent[edit]

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

thm (introduceBiconditionalFromImplicationsInConsequent ()
  ((HFORWARD (antecedent  (p  q)))
   (HREVERSE (antecedent  (q  p))))
  (antecedent  (p  q)) (
        HFORWARD
        HREVERSE
        composeConjunction

        p q BiconditionalImplication eliminateBiconditionalForward

        applySyllogism
))

thm (eliminateBiconditionalReverseInConsequent ()
  ((HIMP (antecedent  (p  q))))
  (antecedent  (p  q)) (
        HIMP
        p q BiconditionalReverseElimination
        applySyllogism
))

thm (eliminateBiconditionalForwardInConsequent ()
  ((HIMP (antecedent  (p  q))))
  (antecedent  (q  p)) (
        HIMP
        p q BiconditionalForwardElimination
        applySyllogism
))

thm (applyModusPonensInConsequent ()
  ((H (antecedent  p))
   (HIMP (antecedent  (p  q))))
  (antecedent  q) (
        H
        HIMP
        composeConjunction

        p q ModusPonens

        applySyllogism
))

thm (applyBiconditionalTransitivityInConsequent ()
  ((H1 (antecedent  (p  q)))
   (H2 (antecedent  (q  r))))
  (antecedent  (p  r)) (
        H1
        H2
        composeConjunction

        p q r BiconditionalTransitivity

        applySyllogism
))

thm (introduceAntecedentInConsequent () ((H (antecedent  p))) (antecedent  (q  p)) (
        H
        p q AntecedentIntroduction
        applySyllogism
))

thm (importInConsequent ()
  ((H (antecedent  (p  (q  r)))))
  (antecedent  ((p  q)  r)) (
        H
        p q r Transportation eliminateBiconditionalReverse
        applySyllogism
))

thm (exportInConsequent ()
  ((H (antecedent  ((p  q)  r))))
  (antecedent  (p  (q  r))) (
        H
        p q r Transportation eliminateBiconditionalForward
        applySyllogism
))

thm (eliminateLeftConjunctInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  q) (
        H
        p q ConjunctionLeftElimination
        applySyllogism
))

thm (eliminateRightConjunctInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  p) (
        H
        p q ConjunctionRightElimination
        applySyllogism
))

thm (introduceTranspositionInConsequent ()
  ((H (antecedent  (p  q))))
  (antecedent  ((¬ q)  (¬ p))) (
        H
        p q TranspositionIntroduction
        applySyllogism
))

Theorems partly in the consequent[edit]

thm (introduceLeftConjunctToConsequent () ((HIMP (antecedent  p)) (HNEW q)) (antecedent  (q  p)) (
        HNEW
        antecedent introduceAntecedent

        HIMP

        composeConjunction
))

thm (introduceRightConjunctToConsequent () ((HIMP (antecedent  p)) (HNEW q)) (antecedent  (p  q)) (
        HIMP

        HNEW
        antecedent introduceAntecedent

        composeConjunction
))

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.

thm (importInAntecedent ()
  ((H ((p  (q  r))  consequent)))
  (((p  q)  r)  consequent) (
        p q r Transportation eliminateBiconditionalForward
        H
        applySyllogism
))

thm (exportInAntecedent ()
  ((H (((p  q)  r)  consequent)))
  ((p  (q  r))  consequent) (
        p q r Transportation eliminateBiconditionalReverse
        H
        applySyllogism
))

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.

The first one swaps the second and third disjuncts in a disjunction of four formulas.[2]

thm (Disjunction4 () () (((p  q)  (r  s))  ((p  r)  (q  s))) (
        p q (r  s) DisjunctionAssociativity

        q r s DisjunctionAssociativity swapBiconditional
        p buildDisjunctionLL
        applyBiconditionalTransitivity

        q r DisjunctionCommutativity
        s buildDisjunctionRR
        p buildDisjunctionLL
        applyBiconditionalTransitivity

        r q s DisjunctionAssociativity
        p buildDisjunctionLL
        applyBiconditionalTransitivity

        p r (q  s) DisjunctionAssociativity swapBiconditional
        applyBiconditionalTransitivity
))

thm (swap23ofDisjunction4 () ((H ((p  q)  (r  s)))) ((p  r)  (q  s)) (
        H
        p q r s Disjunction4
        eliminateBiconditionalReverse
        applyModusPonens
))

thm (Disjunction3 () () (((p  q)  r)  ((p  r)  q)) (
        p q r DisjunctionAssociativity

        q r DisjunctionCommutativity
        p buildDisjunctionLL
        applyBiconditionalTransitivity

        p r q DisjunctionAssociativity
        swapBiconditional
        applyBiconditionalTransitivity
))

thm (swap23ofDisjunction3 () ((H ((p  q)  r))) ((p  r)  q) (
        H
        p q r Disjunction3
        eliminateBiconditionalReverse
        applyModusPonens
))

The next theorem swaps the second and third conjuncts in a conjunction of four formulas.[3]

thm (Conjunction4 () () (((p  q)  (r  s))  ((p  r)  (q  s))) (
        p q (r  s) ConjunctionAssociativity

        q r s ConjunctionAssociativity swapBiconditional
        p buildConjunctionLL
        applyBiconditionalTransitivity

        q r ConjunctionCommutativity
        s buildConjunctionRR
        p buildConjunctionLL
        applyBiconditionalTransitivity

        r q s ConjunctionAssociativity
        p buildConjunctionLL
        applyBiconditionalTransitivity

        p r (q  s) ConjunctionAssociativity swapBiconditional
        applyBiconditionalTransitivity
))

Done[edit]

We now export Interface:Intuitionistic propositional logic.

export (PROPOSITIONAL Interface:Intuitionistic_propositional_logic () ())

Footnotes[edit]

  1. mtbiri, metamath's set.mm, accessed July 20, 2010
  2. or4, metamath's set.mm, accessed February 5, 2011
  3. an4, metamath's set.mm, accessed February 5, 2011

Proof module parsed successfully