5
$\begingroup$

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?

Improve this question
$\endgroup$
15
  • 1
    $\begingroup$ 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. $\endgroup$
    – Erfan Khaniki
    Commented Jan 18, 2016 at 10:07
  • 2
    $\begingroup$ 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). $\endgroup$
    – Carl Mummert
    Commented Jan 18, 2016 at 11:33
  • 2
    $\begingroup$ @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"). $\endgroup$
    – Carl Mummert
    Commented Jan 18, 2016 at 11:34
  • 2
    $\begingroup$ 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) $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Feb 4, 2016 at 17:07
  • 2
    $\begingroup$ 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. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Feb 4, 2016 at 17:12

1 Answer 1

Reset to default
1
+50
$\begingroup$

I share Vladimir Kanovei's view that the syntactical approach might be a good oppportunity to constructive NSA in much the same way as it was for Nelson's Internal Set Theory.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .