The multi-valued Markov's principle

[andrej...@andrej.com]

Dear all,

has anyone come across the following version of Markov’s principle, which I call the multi-valued Markov principle?

Let φ, ψ be predicates on ℕ such that ∀ n . φ(n) ∨ ψ(n). Consider the principle:

¬ ¬ (∃ n . φ(n) ∧ ¬ ψ(n)) ⇒ ∃ n . φ(n) (MVMP)

This is a form of Markov’s principle, and as far as I can tell it is not equivalent to the usual Markov principle.

To explain the name, observe that MVMP is equivalent to the following. Let f : ℕ → P({0,1}) be a multi-valued binary sequence, i.e., for each n ∈ ℕ the set f(n) is inhabited. Consider the principle:

¬ ¬ (∃ n . {1} = f(n)) ⇒ ∃ n . 1 ∈ f(n)

If countable choice holds then Markov principle and multi-valued Markov principle are equivalent, which may be a reason why nobody came across MVMP before.


I have come across the principle while writing up the construction of a topos with countable reals. In that topos, Markov principle seems to fail, but the above principle holds.

With kind regards,

Andrej

[andrej...@andrej.com]

> I have come across the principle while writing up the construction of a topos with countable reals. In that topos, Markov principle seems to fail, but the above principle holds.

Addendum: the above claim about the topos must be false, as Yannick Forster kindly pointed out to me privately that MVMP obviously implies MP.

What I wanted to say, I suppose, was that I needed MVMP because I did not have countable choice and therefore could not extract a function from a statement of the form ∀ n ∈ ℕ . ∃ b ∈ {0,1} . ρ(n, b). (Such a function would be needed for an application of MP, but with MVMP I can work with ρ directly.)

With kind regards,

Andrej

[Andrew Swan]

To show MVMP is strictly stronger than MP, note that MVMP implies the analytic version of MP for Dedekind reals. Then MP holds in the topos of sheaves on the closed unit interval (or any locally connected space), but analytic MP fails.

Best,

Andrew