Completeness if IHOL

[Andrej Bauer]

Dear all,

George Cherevichenko asked a question on MathOverflow (https://mathoverflow.net/q/512959/1176) whether
higher-order intuitionistic logic (IHOL) is complete for certain classes, such as

1. Grothendieck toposes
2. Heyting-valued sets
3. Toposes of topological sheaves
4. Toposes of presheaves (Set^C where C is a small category)
5. Kripke models (Set^C where C is a p.o. set)

By IHOL we mean here the calculus described in, say, Labek & Scott’s book. The book also shows that IHOL is complete for elementary toposes. But what about these restricted classes?

The best I could come up with was pointing to a paper by Steve Awodey and Carsten Butz, which however establishes completenes of *classical* HOL for toposes of topological sheaves.

I am not aware of any references settling the question. On the other hand, it’s a very natural question to ask, so someone must have thought about it. Can someone shed some light on the matter?

With kind regards,

Andrej