Return to Question

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?

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?

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?

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?