Enumeration: Rules of Inference for Intuitionistic Natural Deduction

Rules of Inference for Intuitionistic Natural Deduction

• Conjunction

  • introduction, ∧I

  • elimination

    • left, ∧E₁

    • right, ∧E₂

• Disjunction

  • introduction

    • left, ∨I₁

    • right, ∨I₂

  • elimination, ∨E

• Implication

  • introduction, →I

  • elimination, →E (MP)

• Negation

  • introduction, ¬I

  • elimination, ¬E

• Truth

  • introduction, TI

• Falsum

  • elimination, ⟘E

• Universal quantification

  • introduction, ∀I

  • elimination, ∀E

• Existential quantification

  • introduction, ∃I

  • elimination, ∃E

CONJUNCTION

A true   B true             A ∧ B true       A ∧ B true
--------------- ∧I          ---------- ∧E₁   ---------- ∧E₂
   A ∧ B true                 A true           B true

 Introduction                        Elimination

DISJUNCTION
                                                  [A]ⁱ true  [B]ʲ true
                                                   ⫶           ⫶
  A true           B true             A ∨ B true   C true     C true
---------- ∨I₁   ---------- ∨I₂       ---------------------------------- ∨Eᵢⱼ
A ∨ B true       A ∨ B true                       C true

          Introduction                             Elimination

IMPLICATION

 [A]¹ true
  ⫶
  B true                           A true   A → B true
----------- →I¹                   --------------------- →E (MP)
A → B true                               B true

Introduction                           Elimination

NEGATION

 [A]¹ true
  ⫶
  p true                          A true    ¬A true
----------- ¬I¹                   ------------------ ¬E (EFQ)
 ¬A true                                C true


Introduction                          Elimination

TRUTH                                 FALSE

                                      ⟘ true
-------- ⟙I                          ------- ⟘E
⟙ true                                C true

TRUTH Introduction               FALSE Elimination

UNIVERSAL QUANTIFICATION

[a/x]A true                           ∀x. A true
------------ ∀Iᵃ                      ------------ ∀E
  ∀x.A true                           [t/x]A true

Introduction                          Elimination

EXISTENTIAL QUANTIFICATION


                                       [[a/x]A true]
                                             ⫶
[t/x]A true              ∃x.A true        C true
------------ ∃I          ----------------------------- ∃Eᵃ
  ∃x.A true                        C true

Introduction                    Elimination