If every subset of N is countable, does excluded middle follow?

[andrej...@andrej.com]

Dear all,

in another episode of dispelling the idea that in constructive mathematics all maps are computable (https://cstheory.stackexchange.com/a/52582/705) the following question came up:

Does excluded middle follow from the statement “every subset of ℕ is countable“?

A set S is said to be countable when there is a surjection ℕ → 1 + A.

In a paper with Andrew Swan (Prop. 2.6 of https://arxiv.org/pdf/1804.00427.pdf) we showed that excluded middle follows under the additional assumption of Markov’s principle. Briefly, the argument goes as follows:

It suffices to show for an arbitrary truth value p that it is ¬¬-stable, i.e., ¬¬p ⇒ p.
Let S = { n ∈ ℕ ∣ n = 0 ∨ p} and let e : ℕ → S be an enumeration of S, which exists by assumption. Then p ⇔ ∃ k ∈ ℕ. f(k) ≠ 0, therefore by Markov's p is ¬¬-stable.

An observation worth making is that the function realizability topos RT(K₂) validates the following *external* statement: every subobject of ℕ is decidable, i.e., for any morphism φ : ℕ → Ω, the statement ∀ n : ℕ . φ(n) ∨ ¬φ(n) is valid in the topos (see Prop. 1.1 item (4) of the paper). From this we can deduce the *external* statement “every subobject of ℕ is (internally) countable” (the point of Prop. 2.6 is exactly to show that the internal version is invalid).

Note that the schema “every closed formula φ is equivalent to one of the form ∃ k ∈ ℕ. ψ(k,x), for some decidable proposition ψ(k).“ is sometimes called Kripke’s schema. The stronger variant would be Kripke’s *principle* “∀ p ∈ Ω. ∃ d : ℕ → {0,1}. p ⇔ ∃ k. d k = 1“. Does anyone know a non-classical model of Kripke’s schema or Kripke’s principle?

With kind regards,

Andrej

[R Gutin]

Hi Andrej,

The statement that "every subsingleton is countable" is equivalent to saying that "every proposition is semidecidable".

Markov's principle says that all semidecidable propositions are ¬¬-stable. Since the statement that "all propositions are

¬¬-stable" implies LEM (see footnote [1]), we get LEM.

It seems the role of Markov's principle can be replaced with other axioms governing semidecidable propositions, leading

to different conclusions. For instance, LLPO combined with the statement "all-subsingletons-are-countable" implies WLEM.

Finally, notice that, assuming Countable Choice, the statement that "every subsingleton is countable" is equivalent to

"every subset of N is countable". See footnote [2].

Footnote [1]: Let p be a proposition. It's easy to see that ¬¬(p V ¬p). Use the assumption of ¬¬-stability to cancel to give p V ¬p.

Footnote [2]: One side is trivial. We prove the other. Let S be a subset of N. Let n be in S. Form the set Z(n) = {n} ∩ S. Since

Z(n) is a subsingleton, it's countable by assumption. Countable Choice implies that all countable unions of countable sets are

countable. Notice that S itself is a countable union of countable sets (namely, the Z(n)), so S is countable.

Kind regards,

Ran

--
You received this message because you are subscribed to the Google Groups "constructivenews" group.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/constructivenews/0973238B-1C7A-46A9-914D-CBEA6AEBAA67%40andrej.com.

[R Gutin]

There's a chance these topics might be related:

- SEPARATING FRAGMENTS OF WLEM, LPO, AND MP on JSTOR (especially the one on separating WLEM from other axioms)

- Dehn plane - Wikipedia - You can get subtle violations of Euclidean geometry by introducing infinitesimals into the real numbers

The first one suggests that Non-Standard Analysis, and the idea of Non-Principal Ultrafilters, might help. The second one provides

an interesting route to showing the difference between apartness and inequality in R, which is relevant if we're denying Markov's

principle.

x and y being internally apart could translate to |x - y| being non-infinitesimal externally. x and y being internally non-equal could

translate to x and y being non-equal externally. Then given a line L and a point p not on L, the parallel line L' through p is only unique

if it is *apart* from L everywhere, as opposed to merely unequal.

Assuming CC, Andrej's axiom is equivalent to the statement that all propositions are semidecidable. A semidecidable proposition is

one logically equivalent to some element of 2^N admitting a 1 in its image. If N is the set of Non-Standard natural numbers, then the

truth value p could correspond to the 1 being found at finite n, and the truth value ¬¬p could correspond to the 1 being found at perhaps

infinite n.

I'm not sure if I should be sharing this with you, given that I don't know how to make these intuitions rigorous.

Kind regards,

Ran

[Douglas Bridges]

I think you'll find that the answer to the initial question in this thread has been known for many years to practitioners of constructive analysis. I'd use the set

{x:x=1 and (p or not p)}

Douglas

Douglas Bridges - Chat @ Spike

To view this discussion on the web visit https://groups.google.com/d/msgid/constructivenews/CADzdHf4ZpdkjKhPZBac4wZFDEVQpS-8qudqccCA0RC63V6mJnw%40mail.gmail.com.

[R Gutin]

I don't understand what question this answers.

Let S be your set. You're suggesting getting a surjection u : Nat -> S. How does this help? Also, did you see Andrej's MO post?

[R Gutin]

Er, that was a surjection to 1+S. Sorry.

[Douglas Bridges]

My confusion, sorry. I was thinking of the trivial proof that every subsingleton of omega is finitely enumerable.

Bob Alps and I have this theorem in our book Morse Set Theory, a Foundation for Constructive Mathematics (almost finished):

     The following are equivalent:

       a)   MP + every subset of omega is countable.

       b)   LEM

       c)   every subset of a countable set is countable.

We use 'countable' in the standard sense in constructive analysis: there exists a mapping of a detachable subset A of omega onto the set. To prove that a) implies b), we use the set {n in omega: p or not p}.

Douglas

Douglas Bridges - Chat @ Spike

[andrej...@andrej.com]

Dear Douglas,

your excellent answer resolves all questions, thanks.

(Incidentally, we’re using the same definition of countable, just phraased differently.)

> Bob Alps and I have this theorem in our book Morse Set Theory, a Foundation for Constructive Mathematics (almost finished):
>
> The following are equivalent:
>
> a) MP + every subset of omega is countable.
>
> b) LEM
>
> c) every subset of a countable set is countable.
>
> We use 'countable' in the standard sense in constructive analysis: there exists a mapping of a detachable subset A of omega onto the set. To prove that a) implies b), we use the set {n in omega: p or not p}.

Ah, yes. The set cannot be empty, but since it is countable MP will guarantee it to be inhabited. Very nice.

With kind regards,

Andrej

[R Gutin]

How does c) imply a)?

Kind regards,

Ran

--
You received this message because you are subscribed to the Google Groups "constructivenews" group.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/constructivenews/85EE21E2-0683-4FF0-9756-940DCD10099D%40andrej.com.

[Toby Bartels]

Have we established though that

d) every subset of omega is countable

is definitely weaker?

I thought that was the original question, and I don't see that answered here.

> --
> You received this message because you are subscribed to the Google
> Groups "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to constructivene...@googlegroups.com.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/constructivenews/85EE21E2-0683-4FF0-9756-940DCD10099D%40andrej.com.

[Douglas Bridges]

C) should, of course, have included 'MP'.

Douglas Bridges - Chat @ Spike

To view this discussion on the web visit https://groups.google.com/d/msgid/constructivenews/CADzdHf4EZqQ3NgZNyNCoc-TVX_TYecQMcoZXLDfwkLObmNQ0rw%40mail.gmail.com.

[andrej...@andrej.com]

> d) every subset of omega is countable
>
> is definitely weaker?
>
> I thought that was the original question, and I don't see that answered here.

Indeed it was!

What we know now is that a non-classical model of “every subset of ℕ is countable” cannot validate Markov’s principle, or anything that implies it.

[Andrew Swan]

I think there's actually a few examples of Grothendieck toposes where Kripke's principle holds. Let T be any topological space such that any open set is a countable union of clopen sets, e.g. Cantor space or Baire space, and then consider sheaves on T.

A subobject of 1 is an open set U of T. If U is the union of clopens C_i for i in N, we can define a map f : N -> 2 by setting [[f(i) = 1]] := C_i and [[f(i) = 0]] := T\C_i. This gives U = [[\exists i f(i) = 1]].

To show that Kripke's principle holds internally in the topos, it suffices to show that in every slice topos over a representable the "global" version above holds. However, the slice topos on an open set V is  the same as the topos for the space V with subspace topology. However, V satisfies the same condition that every open is a countable union of clopens, so we can apply the argument above.

Best,

Andrew