HackMDNatural 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)
We repeat the calculus above. Add the proof terms.
\(\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$} \]
