---
tags: lean, intuitionistic logic, johanna
---

# Natural Deduction (exercise on proof terms)

We present the calculus of natural deduction for intuitionstic propositional logic twice.

The first version only concerns the logic and allows us to do pen-and-paper proofs.

The second version is an exercise where the reader is asked to add proof terms (=programs) to the rules. These proof terms should be the same as used in the proof assistant Lean.

## Propositions / Types

The calculus of natural deduction of intuitionistic logic.

#### $\wedge$-introduction

$$
\frac{A\quad\quad B}{A\wedge B}
$$

#### $\wedge$-elimination

$$
\frac{A\wedge B}{A}
\quad\quad\quad\quad
\frac{A\wedge B}{B}
$$

#### $\to$-introduction

$$
\frac{\text{Assume $A$ ... prove $B$}}{A\to B}
$$

#### $\to$-elimination

$$
\frac{A \quad\quad A\to B}{B}
$$

#### $\vee$-introduction

$$
\frac{A}{A\vee B}
\quad\quad\quad\quad
\frac{B}{A\vee B}
$$

#### $\vee$-elimination

$$
\frac{A\vee B \quad\quad A\to C \quad\quad B\to C}{C}
$$

#### $\bot$-elimination

$$
\frac{\bot}{A}
$$

#### negation

$$
\text{$\neg A$ is an abbreviation for $A\to\bot$}
$$

## Proofs / Programs (exercise)

Below, $x$ is a variable and $a,b,f,p$ are expressions (programs, proofs).

**$\wedge$-introduction** [^andIntro]

$$
\frac{a:A\quad\quad b:B}{\langle a,b \rangle: A\wedge B}
$$

[^andIntro]: Write $\langle a,b\rangle$ as `\langle a, b\rangle` and $\wedge$ as `\wedge`

**$\wedge$-elimination** [^andElim]

$$
\frac{\langle a,b\rangle :A\wedge B}{a:A}
\quad\quad\quad\quad
\frac{\langle a,b\rangle :A\wedge B}{b:B}
$$

[^andElim]: We write the elimination using the constructor $\langle -,-\rangle$ and pattern matching. But it is worth noting that elimination rules do come with eliminators or deconstructors and the elimination rules can also be written as
$$
\frac{p:A\wedge B}{p\text{.left}:A}
\quad\quad\quad\quad
\frac{p:A\wedge B}{p\text{.right}:B}
$$

#### $\to$-introduction

$$
\frac{x:A \quad\quad e:B}{\lambda a.b: A\to B}
$$

#### $\to$-elimination

$$
\frac{a:A \quad\quad f:A\to B}{f\,a :B}
$$

#### $\vee$-introduction

$$
\frac{a:A}{A\vee B}
\quad\quad\quad\quad
\frac{b:B}{A\vee B}
$$

#### $\vee$-elimination

$$
\frac{A\vee B \quad\quad A\to C \quad\quad B\to C}{C}
$$

#### $\bot$-elimination

$$
\frac{\bot}{A}
$$

#### negation

$$
\text{$\neg A$ is an abbreviation for $A\to\bot$}
$$