# Constructive compactness for countable models?

The compactness theorem for countable (Tarski?) models is equivalent to the weak König's lemma by a result of H. Friedman and others as noted here, in the context of classical logic. The weak König's lemma in constructive mathematics has been extensively studied as noted here. What is the status of the compactness theorem for countable models itself in constructive mathematics.

One relevant paper seems to be Moerdijk, Ieke; Palmgren, Erik. Minimal models of Heyting arithmetic. J. Symbolic Logic 62 (1997), no. 4, 1448–1460.

One relevant issue is the mutual relation of the following three items:

(1) compactness theorem for countable models;

(2) weak Koenig's lemma;

(3) lesser limited principle of omniscience (LLPO).

In what constructive setting are these principles equivalent? More specifically: how much of the proof of equivalence sketched in the answer to this question can be retained in a suitable constructive setting, using references mentioned in the answer to this question?

• There are different frames for models of intutionistic logic, like kripke model, beth model and a model theory in real line. So you should specify what do you mean by countable model. – Erfan Khaniki Jan 18 '16 at 10:07
• The compactness theorem is a classical theorem about classical models. It would be very unusual for someone in constructive mathematics to worry about such a result. On one hand, constructivists such as Bishop avoid formalization entirely, and thus also avoid model theory. Bishop's interest, essentially, is core math only. On the other hand, constructive metamathematics is done with alternative kinds of models that are relevant to constructive logic. The concept of a model (in the sense of classical model theory) has classical logic through and through (e.g. in the T-schema). – Carl Mummert Jan 18 '16 at 11:33
• @Noah Schweber: in a professional context of logic, I would read "constructive" to mean something like "in intuitionistic logic", rather than the weaker informal meaning that some mathematicians use for it (e.g. "provable in ZF"). – Carl Mummert Jan 18 '16 at 11:34
• I don’t know the answer, I’m afraid; but unlike other commenters, I think this is a good and well-posed question. Formal constructive reverse mathematics has been investigated by e.g. Ishihara, Nemoto, and colleagues, who have certainly considered what intuitionistic formal systems are required for equivalences between WKL, LLPO, and related principles; I have heard several conference talks by them on such issues, though I don’t remember their results precisely. (cont’d) – Peter LeFanu Lumsdaine Feb 4 '16 at 17:07
• On the other hand, while constructive model theory casts its net much wider than classical model theory (including Kripke models and much more), it certainly includes ordinary “Tarski” models as a special case of these. So there is no problem with speaking of “compactness for (countable) (Tarski) models”. The reason Tarski models are less-studied constructively isn’t because they’re problematic, it’s just that there may not exist enough of them for completeness, so one is forced (no pun intended) to look at more general kinds of models. – Peter LeFanu Lumsdaine Feb 4 '16 at 17:12