Lecture 13: Natural Deduction

In this lecture we shift focus from the domain of programming languages to the domain of logic. As before, the overall goal is to use the logical framework LF as a represention language with the difference that the objects under investigations are now logics. In this lecture we concentrate the discussion on one particular logic, i.e. first-order logic, and one particular deductive system to define evidence, i.e. the natural deduction calculus.

Natural deductions are defined by a system of elimination and introduction rules. Based on a guiding design principle, the two classes of rules are dual to each other in the sense that when combining them appropriately information is neither being lost nor gained.

Suggested Reading Materials:

Frank Pfenning. Computation and Deduction, Chapter 7

Alternatively, Natural Deduction is a more recent document that describes local reduction and local expansion in detail.