What Little We Know About Interpretations over Heyting Arithmetic
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!.