Abstract

We show how normalisation (or cut-elimination) results can be obtained from completeness proofs for a certain class of models. I.e. from the constructive proof of completeness of Kripke models we obtain normalisation for minimal logic (or simply typed lambda calculus). To deal with disjunctions (or coproducts) we introduce a version of Beth models (or proof-irrelevant sheaf models). We show then how to obtain normalisation for full propositional intuitionistic logic from completeness for (some version of) Beth models.

Most of the development has been formalized in Type Theory using ALF (Gothenburg) and LEGO (Edinburgh).

This is based on joint work with Martin Hofmann and Thomas Streicher and on inspiration from Thierry Coquand.