Albert Visser

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:

  1. What is an interpretation?
  2. What is a consistency statement?
  3. How to get the effect of induction when you don’t have induction. An introduction to the method of definable cuts.
  4. Proof of the GHBWHF Theorem.
  5. Consequences of the GHBWHF Theorem.