Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: non-Boolean topos where every proposition is semi-decidable

Madeleine Birchfield (Jul 08 2024 at 02:52):

Are there any examples of non-Boolean toposes where every proposition in the internal logic is semi-decidable?

Morgan Rogers (he/him) (Jul 08 2024 at 08:15):

Please can you specify what you mean by semi-decidable? I suspect that toposes of monoid actions will be an answer (or that I will be able to provide such a topos that does, if it's not true in general) but it depends what the "semi" does.

Tom de Jong (Jul 08 2024 at 08:55):

One possible rephrasing is: Is there a topos that validates the (strong) Brouwer-Kripke Schema?

Morgan Rogers (he/him) (Jul 08 2024 at 09:29):

Alright, I'm not sure if the internal collection of binary sequences should be $\N \to 2$ or $\N \to \Omega$; I'll assume the former for now. The collection of binary sequences which are $1$ somewhere is a subobject of the exponential object $[\N,2]$; I'll use $s: S \rightarrowtail [\N,2]$ for that. If I'm interpreting correctly, the KS described on that nLab page says that this should be a weak subobject classifier, in the sense that for any $A \subseteq X$ (interpreting a formula $\phi$) there exists a not-necessarily-unique function $\chi_A: X \to [\N,2]$ such that $A$ is the pullback of $s$ along $\chi_A$. Does that seem right so far?

Madeleine Birchfield (Jul 08 2024 at 10:00):

Morgan Rogers (he/him) said:

Please can you specify what you mean by semi-decidable? I suspect that toposes of monoid actions will be an answer (or that I will be able to provide such a topos that does, if it's not true in general) but it depends what the "semi" does.

A semi-decidable proposition $p$ is defined in Andrej Bauer's Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem as one which satisfies

$$\exists f \in 2^\mathbb{N}.(p \iff \exists n \in \mathbb{N}.f(n) = 1)$$

Madeleine Birchfield (Jul 08 2024 at 10:03):

Another rephrasing is that the Rosolini dominance and the set of truth values coincide.

Madeleine Birchfield (Jul 08 2024 at 10:13):

Morgan Rogers (he/him) said:

Alright, I'm not sure if the internal collection of binary sequences should be $\N \to 2$ or $\N \to \Omega$; I'll assume the former for now.

In toposes which are not boolean, binary sequences are elements of the exponential $2^\mathbb{N}$; elements of $\Omega^\mathbb{N}$ are subobjects of the natural numbers.

Morgan Rogers (he/him) (Jul 08 2024 at 10:54):

I guessed correctly. Some people use "booleans" as shorthand for "truth values" so I wasn't certain.
So we're asking that the function $\exists n.(f(n) = 1) :2^{\N} \to \Omega$ be an epimorphism?

Andrew Swan (Jul 08 2024 at 11:08):

For sheaves on topological spaces, this says that every open set is a countable union of clopen sets, which holds for Cantor space, for example, and sheaves on Cantor space is not boolean.

Madeleine Birchfield (Jul 08 2024 at 13:42):

Morgan Rogers (he/him) said:

So we're asking that the function $\exists n.(f(n) = 1) :2^{\N} \to \Omega$ be an epimorphism?

I think so, because when the codomain is restricted to the Rosolini dominance, the function is an epimorphism.

Morgan Rogers (he/him) (Jul 08 2024 at 14:09):

For presheaves on $\mathcal{C}$, $2^\N (c) = \hat{\mathcal{C}}(\N \times h_c, 2) = \N \times \hat{\mathcal{C}}(h_c,2) = \N \times 2$ is the ordinary set of $\N$-indexed binary sequences, just because both $\N$ and $2$ are constant presheaves, so they can't see any non-complemented parts of $\Omega$. So for presheaf toposes at least, satisfying KS implies Booleanness

Madeleine Birchfield (Jul 08 2024 at 14:56):

If a topos satisfies both KS and LPO for natural numbers (i.e. every semi-decidable proposition is decidable), then the topos is Boolean.

Andrew Swan (Jul 08 2024 at 15:01):

Yes - in fact Markov's principle is enough in place of LPO (this is related to Proposition 2.6 in https://arxiv.org/pdf/1804.00427)

Tom de Jong (Jul 08 2024 at 15:18):

Indeed, that KS + MP -> EM was atributed to Joan Moschovakis (1980) in van Atten (2018).

Chris Grossack (they/them) (Jul 08 2024 at 19:02):

This gives another perspective on Morgan's response too, since presheaf topoi always satisfy LPO (and so satisfy MP too). In fact, the proof that presheaf topoi satisfy LPO is basically what Morgan wrote, haha.

Morgan Rogers (he/him) (Jul 08 2024 at 20:13):

Sometimes I'm reminded in these discussions that I satisfy LPO... :stuck_out_tongue_wink:

dusko (Jul 08 2024 at 21:28):

Madeleine Birchfield said:

Morgan Rogers (he/him) said:

Please can you specify what you mean by semi-decidable? I suspect that toposes of monoid actions will be an answer (or that I will be able to provide such a topos that does, if it's not true in general) but it depends what the "semi" does.

A semi-decidable proposition $p$ is defined in Andrej Bauer's Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem as one which satisfies

$$\exists f \in 2^\mathbb{N}.(p \iff \exists n \in \mathbb{N}.f(n) = 1)$$

Markov's principle implies that a semidecidable $p$ must satisfy $\neg\neg p \implies p$. in realizability toposes, semidecidable objects are thus always at least separated, since the Markov principle holds. the classifier $\Sigma$ of semidecidable objects has been extensively studied in the 90s in various people's theses. when does it coincide with $\Omega$, i don't remember. something should have to be degenerate, since $\Sigma$ is realized by $\cal K$, the halting set, and its complement.

re the monoid actions, phil mulry's thesis was about doing computability theory in the topos of canonical sheaves over the monoid of recursive (total computable) functions. there is a lot of interesting stuff there, but it is a grothendieck topos, which means that it is completed under colimits of diagrams that are not computable or effectively presented. in a sense, mulry's topos is not a topos of computable functions, but a topos of functions that preserve computable (semidecidable) sets. the whole research program of realizability toposes emerged from such considerations: effective toposes are basically the exact completions of the universes of semidecidable (computable) sets given by enumerations... a very important question, in any case, surely with an important future whether we remember the past or reconstruct it :)

dusko (Jul 08 2024 at 21:35):

sorry, i wrote all of the above without knowing what is LPO. so maybe i am saying things which trivially follow from what was said. sorry about that.

but what is LPO?

Madeleine Birchfield (Jul 08 2024 at 21:46):

The limited principle of omniscience (LPO) for the natural numbers says that given any function $f$ from $\mathbb{N}$ to the set $\{0, 1\}$ with two elements, the existential quantifier $\exists x \in \mathbb{N}.f(x) = 1$ is decidable; i.e.

$$(\exists x \in \mathbb{N}.f(x) = 1) \vee \neg (\exists x \in \mathbb{N}.f(x) = 1)$$