nLab semidecidable proposition

 Definition

A proposition or truth value $P$ is semi-decidable or semidecidable if and only if there exists a sequence of booleans $f \in 2^\mathbb{N}$ such that $P$ if and only if there exists a natural number $x \in \mathbb{N}$ such that $f(x) = 1$.

$$\mathrm{isSemiDecidable}(P) \coloneqq \exists f \in 2^\mathbb{N}.P \iff \exists x \in \mathbb{N}.f(x) = 1$$

Equivalently, a proposition or truth value $P$ is semi-decidable or semidecidable if and only if there exists a decidable subset $Q$ of the natural numbers $\mathbb{N}$ such that $P$ if and only if there exists a natural number $x \in \mathbb{N}$ such that $Q(x)$.

$$\mathrm{isSemiDecidable}(P) \coloneqq \exists Q \in \mathcal{P}(\mathbb{N}).\mathrm{isDecidable}(Q) \wedge (P \iff \exists x \in \mathbb{N}.x \in Q)$$

where a subset $Q$ is decidable if and only if for all $x \in \mathbb{N}$, $x \in Q \vee x \notin Q$.

Semidecidability structures

One can also consider propositions having the structure of a sequence of booleans where one of the booleans in the sequence is true, rather than there existing a sequence of booleans where one of the booleans in the sequence is true.

Definition

A semidecidability structure (de Jong 2021) or a Rosolini structure (Escardo & Knapp 2017) on a proposition $P$ is a sequence $f$ of booleans such that $P$ if and only if there exists a natural number $x \in \mathbb{N}$ such that $f(x) = 1$.

The set of semidecidability structures on a proposition $P$ is given by the set

$$\{f \in 2^\mathbb{N} \vert P \iff \exists x \in \mathbb{N}.f(x) = 1\}$$

Semidecidability structures are used to define a weak form of choice called Rosolini propositional choice (Escardo & Knapp 2017) or Escardo-Knapp choice (de Jong, Kraus, Mohammadzadeh, & Forsberg 2026), see below.

Set of semi-decidable propositions

The set of all semidecidable propositions $\Sigma_0^1$ is defined as a subset of the set of propositions $\Omega$ containing all the semidecidable propositions:

$$\Sigma_0^1 \coloneqq \{P \in \Omega \vert \exists f \in 2^\mathbb{N}.(P = \top) \iff \exists x \in \mathbb{N}.f(x) = 1$$

In predicative mathematics, the set of all propositions may not exist, so instead in order to construct the set of all semidecidable propositions, we take any sub-$\sigma$-frame of propositions $\Sigma$ and collect the ones that are semidecidable:

$$\Sigma_0^1 \coloneqq \{P \in \Sigma \vert \exists f \in 2^\mathbb{N}.(P = \top) \iff \exists x \in \mathbb{N}.f(x) = 1$$

Such $\sigma$-frames $\Sigma$ are usually found by collecting the subsingletons of a universe of sets $U$ in the theory into a set $\Omega_U$, or minimally, by the set of quasi-decidable truth values defined later in this article.

Constructive taboos

There are a few constructive taboos related to the set of semidecidable propositions.

Rosolini dominance

In classical mathematics and in constructive mathematics which accepts countable choice, every quasidecidable proposition is a semidecidable proposition (Sterling & Ye 2025, de Jong, Kraus, Mohammadzadeh, & Forsberg 2026), and in this case the set of semidecidable propositions is called the Rosolini dominance, since the set of quasidecidable propositions is an $\mathbb{N}$-overt dominance.

However, more generally, one cannot prove that the set of semidecdiable propositions is an $\mathbb{N}$-overt dominance and thus coincide with the set of quasidecidable propositions. That the set of semidecdiable propositions is a dominance is called Rosolini’s dominance axiom (de Jong 2021).

Definition

Rosolini’s dominance axiom states that given a semidecidable proposition $P$, if $P$ implies that a proposition $Q$ is semidecidable, then their conjunction $P \wedge Q$ is semidecidable.

The Rosolini dominance axiom is equivalent to a form of choice called Rosolini propositional choice (Escardo & Knapp 2017) or Escardo-Knapp choice (de Jong 2021, de Jong, Kraus, Mohammadzadeh, & Forsberg 2026), which follows from the propositional axiom of choice.

Definition

Rosolini propositional choice or Escardo-Knapp choice states that given a semidecidable proposition $P$, if $P$ implies that $Q$ is semidecidable, then there merely exists a function from (the corresponding subsingleton of) $P$ to the set of semidecidability structures on $Q$.

See section 2.8 of Escardo & Knapp 2017 and also de Jong 2021 for more details.

Rosolini propositional choice then in turn is equivalent to the statement that every quasidecidable proposition is a semidecidable proposition; see de Jong, Kraus, Mohammadzadeh, & Forsberg 2026 for more details.

LPO and Phoa’s principle

In classical mathematics, and in constructive mathematics which accept the limited principle of omniscience (LPO), the set of semideciable truth values is just the boolean domain $\mathbb{2}$. In fact, we have the following:

Theorem

LPO holds if and only if the set of semideciable propositions coincides with the boolean domain.

Proof

LPO implies that for all sequences $f$ in the boolean domain, the existential quantification $\exists n \in \mathbb{N}, f(n) = 1$ is decidable; hence valued in the booleans. Thus, the boolean domain is closed under existential quantification over the natural numbers. Since the boolean domain is a subset of the set of semideciable propositions, this implies that the boolean domain coincide with the set of semideciable propositions by definition of the set of semideciable propositions.

Conversely, suppose that the booleans coincide with the set of semideciable propositions. Then we have that the existential quantification $\exists n \in \mathbb{N}, f(n) = 1$ is a boolean, which implies LPO.

On the other hand, in synthetic topology and synthetic domain theory, one sometimes sees Phoa's principle or synthetic quasi-coherence assumed for an $\mathbb{N}$-overt dominance, in order to emulate the behavior of Sierpinski space, where every function is monotonic. Under Rosolini propositional choice, the set of semideciable propositions is an $\mathbb{N}$-overt dominance, so it is consistent to assume such axioms for the set of semideciable propositions, such as Phoa's principle for the set of semideciable propositions in the effective topos. Moreover, since the set of semidecidable propositions is a distributive lattice, and Phoa's principle or synthetic quasi-coherence do not rely on the structure of an $\mathbb{N}$-overt dominance, but only on the set of semidecidable propositions being a distributive lattice, such axioms can be assumed of the set of semidecidable propositions even in the absence of Rosolini propositional choice. However, such axioms are inconsistent with LPO:

Theorem

LPO is inconsistent with Phoa's principle for the set of semideciable propositions $\Sigma$.

Proof

LPO is equivalent to the fact that the boolean domain coincides with the set of semideciable propositions. However, the logical negation function $x \mapsto \neg x$ on the boolean domain does not satisfy the linear interpolation condition for Phoa’s principle for the booleans; it is not true that $\neg x = (\neg 1) \wedge (x \vee \neg 0) = 0 \wedge (x \vee 1) = x$ on the booleans. As a result, LPO is inconsistent with Phoa’s principle for set of semideciable propositions.

In traditional point-set topology in classical mathematics, one already has that negation on the booleans is not a continuous function with respect to the Scott topology of the booleans.

Lemma

LPO is inconsistent with synthetic quasi-coherence for the set of semideciable propositions $\Sigma$; that is, let $A$ be a finitely presented $\Sigma$-algebra, in the sense that $A$ is a distributive lattice equivalent to the quotient of $\Sigma[x_1 \ldots x_n]$ by finitely many relations, and let $\mathrm{Spec}_\Sigma(A)$ be the set of $\Sigma$-algebra homomorphisms. Then the canonical lattice homomorphism

$$a \mapsto (f \mapsto f(a)):A \to \Sigma^{\mathrm{Spec}_\Sigma(A)}$$

is an isomorphism

Proof

Synthetic quasi-coherence for the set of semideciable propositions $\Sigma$ implies Phoa's principle for $\Sigma$, and so is thus inconsistent with LPO.

Generalizations

Ordinal decidable propositions

Given an ordinal $\alpha$, there exists a notion of $\alpha$-decidable propositions (de Jong, Kraus, Mohammadzadeh, & Forsberg 2026), where the usual notion of semi-decidable proposition is an $(\omega + 1)$-decidable proposition.

Sierpiński semi-decidable propositions

One can also consider the closure of semi-decidable propositions under existential quantification over the natural numbers; these are the quasi-decidable propositions or the Sierpiński semi-decidable propositions.

Related concepts

• decidable proposition

• proposition, truth value

• quasidecidable proposition

• synthetic topology, synthetic domain theory

• distributive lattice

 References

• Andrej Bauer, First Steps in Synthetic Computability Theory, Electronic Notes in Theoretical Computer Science, volume 155, pages 5–13, 2006. Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI) [doi:10.1016/j.entcs.2005.11.049]

• Andrej Bauer, Davorin Lešnik, Metric Spaces in Synthetic Topology, Annals of Pure and Applied Logic, Volume 163, Issue 2, February 2012, Pages 87-100 [doi:10.1016/j.apal.2011.06.017, pdf]

• Martín Escardó, Cory Knapp?. Partial Elements and Recursion via Dominances in Univalent Type Theory. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) [10.4230/LIPIcs.CSL.2017.21]

• Tom de Jong. Semidecidable propositions. Agda code with comments, 2021. (URL).

• Jonathan Sterling, Lingyuan Ye, Domains and Classifying Topoi (arXiv:2505.13096)

• Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg, Generalized Decidability via Brouwer Trees (arXiv:2602.10844)