# From Consistency to Interpretability

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.