MMT - 4 - Natural Deduction for Intuitionistic Propositional Logic

4 - Natural Deduction for Intuitionistic Propositional Logic

In this section, we will look at the natural deduction calculus for intuitionistic propositional logic. If you already know the calculus, you can safely skip this section.

Intuitionistic logic is a constructive fragment of classical logic - i.e. syntactically identical, but the law of the excluded middle A ∨ ¬A is omitted.

Natural Deduction calculi follow the idea that we give for each logical connective introduction and elimination rules.

Introduction rules tell us, when we are allowed to introduce an instance of the connective. e.g. the introduction rule for ∧ is pretty straight-forward:

$`\dfrac{\vdash A\quad \vdash B}{\vdash A \wedge B}`$

If A is provable and B is provable, then A∧B is provable.

Conversely, elimination rules allow us to get rid of the connective. In the case of ∧, there are two ways to do that:

$`\dfrac{\vdash A\wedge B}{\vdash A}`$ and $`\dfrac{\vdash A\wedge B}{\vdash A}`$

If A∧B is provable, then A is provable.
If A∧B is provable, then B is provable.

Since we use judgments-as-types, these three rules correspond to the following three function types:

$`\vdash A \to \vdash B \to \vdash A\wedge B`$
$`\vdash A \wedge B \to \vdash A`$
$`\vdash A \wedge B \to \vdash B`$

Noticably, the function arrows in these types lend themselves to be interpreted just like implications: We can read e.g. the first rule as

If A is provable, then (if B is provable, then A∧B is provable).

This is no coincidence - this correspondence between a logical connective and a type constructor is known as Curry-Howard-Isomorphism (or propositions-as-types), and we will (rather trivially) prove this isomorphism later in MMT using views.

However, the types above don’t quite work in LF, for the simple reason, that A and B are free variables. The proof rules are valid for any propositions A, B, so to avoid them being free variables, we can instead declare a function that takes two proposition A,B and returns the functions corresponding to the rules. For that, we finally need the dependend function types:

$`\prod_{A:prop}\prod_{B:prop}\vdash A \to \vdash B \to \vdash A\wedge B`$
$`\prod_{A:prop}\prod_{B:prop}\vdash A \wedge B \to \vdash A`$
$`\prod_{A:prop}\prod_{B:prop}\vdash A \wedge B \to \vdash B`$

Again, noticably, the dependent functions here lend themselves to be read like a “for all” - e.g. we can read the first rule as

For all A:prop, for all B:prop: If A is provable, then (if B is provable, then A∧B is provable).

The Proof Rules

The full set of rules of the natural deduction calculus is:

Symbol	Introduction Rule(s)	Elimination Rule(s)
`⊤`	$`\dfrac{\ }{\vdash\top}`$	None
`⊥`	None	$`\dfrac{\vdash\bot}{\vdash A}`$
`¬`	$`\dfrac{\begin{matrix}[A]\ \vdots \ \vdash\bot\end{matrix}}{\vdash\neg A}`$	$`\dfrac{\vdash A\quad\vdash \neg A}{\vdash\bot}`$
`∧`	$`\dfrac{\vdash A\quad \vdash B}{\vdash A \wedge B}`$	$`\dfrac{\vdash A\wedge B}{\vdash A}`$ and $`\dfrac{\vdash A\wedge B}{\vdash A}`$
`∨`	$`\dfrac{\vdash A}{\vdash A \vee B}`$ and $`\dfrac{\vdash b}{\vdash A \vee B}`$	$`\dfrac{\begin{matrix}[A]\ \vdots\ \vdash C\end{matrix}\quad\begin{matrix}[B]\ \vdots\ \vdash C\end{matrix}\quad\begin{matrix}\ \ \ \ \vdash A\vee B\end{matrix}}{\vdash C}`$
`⇒`	$`\dfrac{\begin{matrix}[A]\ \vdots\ \vdash B\end{matrix}}{\vdash A \Rightarrow B}`$	$`\dfrac{\vdash A\Rightarrow B\quad\vdash A}{\vdash B}`$

> 5 - Structures, Lambda, Pi and Implicit Arguments