Lecture 10: Hypothetical Judgments

In this lecture we discuss how hypothetical judgments can be represented in the logical framework LF. A hypothetical judgment is a judgment whose derivations rely on the possibility to introduce new assumptions.

We demonstrate the concept of hypothetical judgments using an algorithm that determines if an expression is closed. One of the main results of this lecture is, that we can encode hypothetical derivations with higher-order dependent functions in LF.

Suggested Reading Materials:

Frank Pfenning. Computation and Deduction, Chapter 5 - 5.2

Source Code:

closed.elf