Intuitionistic logic

The version of intuitionistic logic presented here is based on natural deduction, and specially emphasises the contraction and weakening rules, which are the key to understanding linear logic.

A proposition is built up from propositional constants using the combining forms implies (->), and (⨉), or (+). Let A,B,C range over propositions, and X range over propositional constants, then the grammar of propositions is as follows:

A,B,C := X | A -> B | A ⨉ B | A + B

An assumption is a sequence of zero or more propositions. Let Γ, ∆, Θ range over assumptions.

A judgement has the form Γ |- A, meaning that from assumptions Γ one can conclude proposition A.

An inference rule consists of zero or more judgements written above a line, and one judgement written below. If all the judgements above the line are derivable, then the judgement below is also derivable.

Therefore, there are 3 different levels of implication: -> in a proposition, |- in a judgement, and the horizontal line in an inference rule.

------ Id
A ⊢ A


Γ, ∆ ⊢ A               Γ, A, A ⊢ B                   Γ ⊢ B
---------- Exchange    ------------ Contraction     -------- Weakening
∆, Γ ⊢ A                 Γ, A ⊢ B                   Γ, A ⊢ B


Γ, A ⊢ B            Γ ⊢ A -> B     ∆ ⊢ A
----------- ->I    ---------------------- ->E
Γ ⊢ A -> B                Γ, ∆ ⊢ B


Γ ⊢ A     ∆ ⊢ B          Γ ⊢ A ⨉ B     ∆, A, B ⊢ C
----------------- ⨉I    -------------------------- ⨉E
  Γ, ∆ ⊢ A ⨉ B                   Γ, ∆ ⊢ C


  Γ ⊢ A             Γ ⊢ B           Γ ⊢ A + B   ∆, A ⊢ C   ∆, B ⊢ C
---------- +I₁   ---------- +I₂     ------------------------------- +E
Γ ⊢ A + B         Γ ⊢ A + B                     Γ, ∆ ⊢ C

Groups of inference rules:

• Axioms

  • Id is the only rule with no judgements above the line. This rule expresses tautology: from hypotheses A one can deduce conclusion A

• Structural rules

  • Exchange expresses that the order of hypotheses is irrelevant

  • Contraction expresses that any hypothesis may be duplicated

  • Weakening expresses that any hypothesis may be discarded

• Logical rules

  • introduction and elimination pairs

  • introduction (->I), a judgement ending in a proposition formed with -> appears below the line

  • elimination rule (->E), a judgment ending in a proposition formed with -> appears above the line

  • Similarly for the other logical connectives, ⨉ and +

Alternative rules for conjunction

Γ ⊢ A    Γ ⊢ B          Γ ⊢ A ⨉ B         Γ ⊢ A ⨉ B
---------------- ⨉I    ----------- ⨉E₁   ----------- ⨉E₂
   Γ ⊢ A ⨉ B              Γ ⊢ A              Γ ⊢ B

These alt conjunction rules may be derived from the ones above, plus Weakening and Contraction. Furthermore, the old rules may be derived from the new, plus Weakening, Contraction, ->I, and ->E.