TobyBartels comments on Exponentiation goes wrong first

[TobyBartels]

my personal favorite higher order logic is the internal language of the free topos

That doesn’t even have a model of PA in it!