< 3 - LF and Judgments-as-Types
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:
If
A
is provable andB
is provable, thenA∧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:
and
If
A∧B
is provable, thenA
is provable.
IfA∧B
is provable, thenB
is provable.
Since we use judgments-as-types, these three rules correspond to the following three function types:
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 (ifB
is provable, thenA∧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:
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 allB:prop
: IfA
is provable, then (ifB
is provable, thenA∧B
is provable).
The full set of rules of the natural deduction calculus is:
Symbol | Introduction Rule(s) | Elimination Rule(s) |
---|---|---|
⊤ |
None | |
⊥ |
None | |
¬ |
||
∧ |
and | |
∨ |
and | |
⇒ |