This tutorial will be entirely devoted to the exposition of a single theorem: the Gödel-Hilbert-Bernays-Wang-Henkin-Feferman Theorem. This theorem is a miniaturization of the Model Existence Lemma. Where the Model Existence Lemma tells us that a consistent theory has a model, the GHBWHF Theorem tells us that if a theory U proves the consistency of another theory V, then U interprets V. So the GHBWHF Theorem is something like the Interpretation Existence Lemma.
The course will be structured as follows:
- What is an interpretation?
- What is a consistency statement?
- How to get the effect of induction when you don’t have induction. An introduction to the method of definable cuts.
- Proof of the GHBWHF Theorem.
- Consequences of the GHBWHF Theorem.