Intuitionistic propositional logic has several kinds of models. Bezhanishvili and Holliday [1] showed that these models form a neat hierarchy:
- Kripke
- Beth
- Topological
- Dragalin
- Heyting
in the order of least general to most general. Kreisel [2] proved that Kripke-completeness implies Markov's principle. Soon, Veldman [3] showed that if we consider Kripke structures with exploding worlds, then completeness is constructive.
Has the constructivity of proving completeness been explored in the other aforementioned semantics?
My intuition is that the more general the class of models, the easier it is to construct a countermodel; therefore, weaker non-constructive means should be necessary to establish their existence.
I also think this could depend on how the semantics are presented. For example, depending on whether the topological semantics is presented in a pointfree style or not, the answer could change.
[1] Bezhanishvili and Holliday. A semantic hierarchy for intuitionistic logic (2019)
[2] Kreisel. On weak completeness of intuitionistic predicate logic (1962)
[3] Veldman. An intuitionistic completeness theorem for intuitionistic predicate logic (1976)
