What Little We Know About Interpretations over Heyting Arithmetic
Albert Visser

Very little is known about interpretations over Heyting Arithmetic (HA). We do not even know whether there is a non-trival interpretation of HA in itself.

In this talk, I discuss what we do know. I show that there are only trivial interpretations of i-EA in HA+CT_0!. This surprising fact has several consequences for interpretations in HA and for interpretability over HA. For example, HA has no Orey sentences. HA does not interpret itself plus the Tarski Biconditionals. I show how a principle of the interpretability logic of HA follows from the scarcity of interpretations of i-EA in HA+CT_0!.