Natural Deduction

logic

Definition

Natural Deduction

Natural deduction is a calculus for deriving logical consequences that aims to mimic the way human reasoning naturally proceeds. Unlike Hilbert calculi, it uses few axioms and instead relies on a collection of inference rules for each logical operator.

Properties

• Soundness: Every formula derivable in natural deduction is a tautology.
• Completeness: Every tautology in propositional or first-order logic is derivable in natural deduction.

Intuitionistic vs. Classic

In its original form, natural deduction is used for intuitionistic logic. To obtain classical logic, one must add an additional rule such as the Law of Excluded Middle ($A\vee \neg A$) or Double Negation Elimination ($\neg \neg A⊢A$).

Core Principles

For every logical operator, natural deduction typically provides two types of rules:

1. Introduction Rules ($I$): Specify how to derive a formula containing the operator.
2. Elimination Rules ($E$): Specify how to use a formula containing the operator to derive other formulas.

Assumptions and Discharges

Natural deduction allows for the temporary use of assumptions. An assumption $[A]$ is a premise that is introduced into a sub-proof. If the conclusion of the sub-proof allows it, the assumption is discharged, meaning the final result no longer depends on the truth of $[A]$.

Inference Rules

Conjunction

• Introduction: $\frac{AB}{A\wedge B}{}_{(\wedge I)}$
• Elimination: $\frac{A\wedge B}{A}{}_{(\wedge E_1)}\frac{A\wedge B}{B}{}_{(\wedge E_2)}$

Implication

• Introduction: $\frac{[A]\dots B}{A⟹B}{}_{⟹I}$ (discharges assumption $A$)
• Elimination: $\frac{A⟹BA}{B}{}_{⟹E}$ (Modus Ponens)