Natural Deduction Rules

This page contains the full list of basic inference rules used in the given natural deduction system.

Conjunction Introduction §

$$\frac{\Gamma ⊢A,\Gamma ⊢B}{\Gamma ⊢A\wedge B}$$

Conjunction Elimination §

$$\frac{\Gamma ⊢A\wedge B}{\Gamma ⊢A,\Gamma ⊢B}$$

Disjunction Introduction §

$$\frac{\Gamma ⊢A}{\Gamma ⊢A\vee B}$$

Disjunction Elimination (proof by cases) §

$$\frac{\Gamma ⊢A\vee B,\Gamma ,A⊢C,\Gamma ,B⊢C}{\Gamma ⊢C}$$

Implication Introduction §

$$\frac{\Gamma ,A⊢B}{\Gamma ⊢A\to B}$$

Implication Elimination (modus ponens) §

$$\frac{\Gamma ⊢A,\Gamma ⊢A\to B}{\Gamma ⊢B}$$

Negation Introduction §

$$\frac{\Gamma ,A⊢\perp }{\Gamma ⊢\neg A}$$

Negation Elimination §

$$\frac{\Gamma ⊢A,\Gamma ⊢\neg A}{\Gamma ⊢B}$$

Double Negation Introduction §

$$\frac{\Gamma ⊢A}{\Gamma ⊢\neg \neg A}$$

Double Negation Elimination §

$$\frac{\Gamma ⊢\neg \neg A}{\Gamma ⊢A}$$

Axiom §

$$\frac{}{\Gamma ,A⊢A}$$

Weakening §

$$\frac{\Gamma ⊢B}{\Gamma ,A⊢B}$$