{{header | title = Intuitionistic propositional logic | subtitle = | left = | right = | shortcut = | notes = The purpose of this page is to prove the statements of Interface:Intuitionistic propositional logic from the Interface:Axioms of intuitionistic propositional logic. }} {{interfaces | imports = Interface:Axioms of intuitionistic propositional logic | exports = Interface:Intuitionistic propositional logic }}

We define some variables for well-formed formulas:

Some of the proofs here are adapted, or even entirely copy-pasted, from pages such as Principia Mathematica propositional logic or Standard axioms imply Principia Mathematica axioms. It would be possible to reduce this duplication by having some of the other pages build on Interface:Intuitionistic propositional logic, but the presentation might become less clear in other ways (certainly it would less closely track the way things are developed in ''Principia''), so we do not currently have the intuitionistic tail wag the classical dog.

Some proofs are taken from metamath's set.mm. In particular, metamath's section "Logical implication" makes use only of the two axioms Simp and Frege, and thus is entirely valid in an intuitionistic context.<ref>[http://us.metamath.org/mpeuni/mmtheorems.html#mm2b Propositional calculus], from Metamath Proof Explorer, accessed February 26, 2010</ref>


Rule for antecedent distribution

It will be convenient to have the ''Frege'' axiom as a rule:


Next we derive the syllogism, which allows us to combine several implications.

Implication reflexivity

Any proposition implies itself:

More common operations

Given a nested implication we often want to exchange the two antecedents:

If we have an implication, adding a common term to the antecedent and the consequent yields a new theorem:

The analogous operation adding consequents swaps the initial antecedent and consequent:

Here's a theorem form of applyComm:

Absorb redundant antecedent

We can absorb a redundant antecedent:

Antecedent introduction

We provide another name and a rule form for the Simp axiom:

Converse of antecedent distribution

The converse of the Frege axiom also holds.<ref>[http://us.metamath.org/mpeuni/pm2.86.html pm2.86] in metamath's set.mm, accessed May 14, 2010</ref>

Syllogism in the consequent

This theorem is similar to syllogism, but where each piece has a common antecedent.



If we can prove two propositions, the conjunction of the two follows (this is just a rule form of the ConjunctionRightIntroduction axiom):

Here are rules for the ConjunctionLeftElimination and ConjunctionRightElimination axioms:

Left introduction

Most of the introduction and elimination statements we need to provide are axioms, but this one is a simple consequence of the axioms:

Conjunction composition

Our first major theorem relating conjunction to implication is composition: from p → q and p → r, we can conclude p → (q ∧ r).

We also prove a version of the converse:

Export and import

The import and export theorems from classical propositional logic also hold in intuitionistic logic. We start with export, (p ∧ q → r) → (p → (q → r)). The proof is based around a variant of CommonConsequentAddition which has two antecedents, rather than one.

The proof of export was based around having a conjunction as a consequent, that is p → (q → p ∧ q). The proof of import is based around p ∧ q → p (and likewise for q). The following lemma is what we'll use to glue together the different parts of the proof, and is basically a gussied up variant of applySyllogism:

Implication transitivity and other consequences of import


The form of the syllogism in Interface:Intuitionistic propositional logic is easy now that we have import:

Likewise, we restate ConjunctionComposition1 using the new tool:




Our first major builder lets us add a common conjunct to both sides of an implication. We start with a few lemmas, and then prove the main theorem.

Other builders

The rest of the ConjunctionMultiplication variants follow from the first one, just like in Principia Mathematica propositional logic.


We provide a variation of the disjunction composition axiom, and a rule form:

Here are a few other rules corresponding to axioms.




Our first disjunction builder is proved analogously to ConjunctionMultiplicationRR.


This theorem follows exactly as ConjunctionMultiplication, except that we use DisjunctionSummationRL instead of ConjunctionMultiplicationRR and ConjunctionCommutativity.

DisjunctionSummation variations

We could prove the DisjunctionSummationLL, DisjunctionSummationRR, and DisjunctionSummationLR the same way that we proved DisjunctionSummationRL, but here we prove them as special cases of DisjunctionSummation.


We define the biconditional as the conjunction of two implications:

And one way to prove a biconditional is to prove both of the implications:

We can eliminate one of the implications of a biconditional:

Biconditionalized versions of some theorems we've already proved

We've proved both directions of each of the following theorems, so the biconditional immediately follows:

Reflexive, symmetric, and transitive

The biconditional has these three properties (which correspond to those defining an equivalence relation). The proofs here are taken directly from Principia Mathematica propositional logic, as they are also valid in intuitionistic logic.

Relating biconditional to implications

The following just restate the definition of the biconditional.

Algebraic laws for disjunction and conjunction

Most of the theorems of the propositional calculus which are analagous to those of other algebras, showing properties such as commutivity and associativity, also hold for intuitionistic logic.

Conjunction idempotence

Conjunction commutativity

Conjunction associativity

To prove associativity for conjunctions, (p ∧ q) ∧ r → p ∧ (q ∧ r), we first put onto the proof stack the statements that the left hand side implies each of p, q, and r.

The proof for associating left is similar.

Disjunction idempotence

Disjunction commutativity

Disjunction associativity

Proving associativity for disjunction is very much analogous to conjunction, with conjunction elimination and composition changed to disjunction introduction and composition.


The builders for conjunction and disjunction can be proved using the proofs in Principia Mathematica propositional logic.



This is just like the theorem for conjunction, except that we build on the partial builder theorem DisjunctionSummation instead of ConjunctionMultiplication:


Here we take up distributivity of disjunction over conjunction, and conjunction over disjunction. Most of the proofs given in Principia Mathematica propositional logic apply for intuitionistic logic, as they are fairly straightforward applications of disjunction and conjunction composition. The tough one is ((p ∨ q) ∧ (p ∨ r)) → p ∨ (q ∧ r) (because it has a conjunction in the antecedent and a disjunction in the consequent, it won't yield to straightforward composition tricks). ''Principia'' proves it from the equivalence of p ∨ q and ¬ p → q (which does not hold in both directions in intuitionistic logic). We prove it from import and builders.

The first step is a lemma which will let us harmlessly apply builders more than once.

Now we are ready for the proof of the tough distributivity case.

The rest of this section contains proofs taken from Principia Mathematica propositional logic.

Also from Principia Mathematica propositional logic are commuted versions of both laws and some rules:

Biconditional and conjunction

A true conjunct does not affect the truth of a proposition. The proof from Principia Mathematica propositional logic is valid intuitionistically without change.

Modus Ponens

This is just an implication corresponding to the modus ponens rule:



Although intuitionistic logic does not allow removing transposition, it does allow introducing it.

Modus tollens is an easy consequence of transposition introduction.

Double Negation

Double negation introduction follows fairly directly from our first negation axiom.

Triple negation

In intuitionistic logic, ¬ ¬ p is not equivalent to p itself. Triple negation, however, is equivalent to single negation, so one merely needs to worry about formulas without negation, with single negation, or with double negation, not greater amounts of negation.

Disjunctive syllogism

Disjunctive syllogism:

DeMorgan's laws

The first two of DeMorgan's laws are straightforward:

To prove the converse of NegationDistributionPDP, we start with a lemma which is a rearrangement of DisjunctiveSyllogism plus transposition.

This lemma is, however, just an import away from the desired result.

Combining the forward and reverse directions we get NegationCollectionNCNDistributionPDP:

The following result follows from double negation introduction and NegationCollectionNCNDistributionPDP.

We can pull the same trick for disjunction to get our final version of DeMorgan's law.


Double negation and connectives

The first two of these relationships between double negation and conjunction or disjunction are easy consequences of transposition.

The converse of DoubleNegatedConjunctionReverse we can prove via the following lemma which introduces double negation to all three formulas of a nested implication.

No contradictions

The Explosion axiom amounts to denying that a proposition and its negation can both hold. Here we express this idea as a theorem (which is also found as *3.24 in Principia Mathematica propositional logic).

Case elimination

Proving a theorem by cases, as in CaseElimination of Interface:Classical propositional calculus, is not, in general, allowed in intuitionism/constructivism. For example, there is a well-known non-constructive proof that an irrational number raised to an irrational power can be rational that proceeds by handling the cases where √2<sup>√2</sup> is rational or irrational, without establishing which one holds. A constructive proof, on the other hand, would need to establish whether √2<sup>√2</sup> was rational first.<ref>Su, Francis E., et al. "http://www.math.hmc.edu/funfacts/ffiles/10004.3-5.shtml Rational Irrational Power," http://www.math.hmc.edu/funfacts Mudd Math Fun Facts, accessed 3 Jul 2010</ref> We do note that p ∨ q, which is stronger than ¬ p → q in intuitionistic logic, can be used for case elimination. This is more of a curiosity than a way of proving anything, as proving p ∨ q in intuitionistic logic would tend to be as hard as proving q.

More builders

Now that we've proved some results involving negation, we are ready to tackle the rest of the builders.


The negation builder is an easy consequence of transposition introduction (we just need to biconditionalize it).


The proof of the implication builder is analogous to the way we proved ConjunctionMultiplication. We base it on CommonConsequentAddition and CommonAntecedentAddition.


We derive the biconditional builder from the implication builder, just as in Principia Mathematica propositional logic.

Distribution of implication over biconditional

The proof of this result from Principia Mathematica propositional logic applies verbatim.

Relationships between connectives

Conjunction and implication

Analogous to DeMorgan's law, there are four relationships between conjunction and implication, which differ depending on where the negations are placed. They are: p ∧ q → ¬ (p → ¬ q) (p → q) → ¬ (p ∧ ¬ q) p ∧ ¬ q → ¬ (p → q) p → ¬ q ↔ ¬ (p ∧ q)

For now, we only prove the third one.

Disjunction and implication

The following implication/disjunction theorems are easy consequences of this one.

The converse of NotDisjunctionImplicationReverse also holds, but is a bit more difficult.

Proving a biconditional from two disjunctions

Since a suitably negated disjunction implies an implication, the antecedent of this theorem readily reduces to p → q and q → p, which is what we need to prove p ↔ q.

True and false connectives

We already defined true (⊤) in Axioms of intuitionistic propositional logic. We define false (⊥) as ¬ ⊤.

The Contradiction theorem also holds. To prove it the same way as TautologyId would require ¬ p ∧ ¬ q → (p ↔ q) (*5.21 in Principia Mathematica propositional logic). We don't have that, but Contradiction follows without too much trouble from Explosion.

Negation and ⊥

Here we show that ¬ p is equivalent to p → ⊥. In some axiomizations of intuitionistic logic, this is the definition of negation. For us, it is a theorem.


We have proved everything in Interface:Basic intuitionistic propositional logic. There are additional theorems in Interface:Intuitionistic propositional logic, but those are proved in Convenience theorems of intuitionistic propositional logic.


<references />


Login to edit