nLab quasidecidable proposition

Idea

Semi-decidable propositions are not closed under existential quantification over the natural numbers: Given a predicate $P$ over the natural numbers where each $P(n)$ is semi-decidable for all $n \in \mathbb{N}$, the existential quantifier $\exists n \in \mathbb{N}.P(n)$ is not always semi-decidable. The closure of semi-decidable propositions under the logical operations of finite conjunctions and existential quantification over the natural numbers are the quasidecidable propositions (Escardo 2020) or Sierpiński semidecidable propositions (de Jong, Kraus, Mohammadzadeh, & Forsberg 2026).

The set of quasidecidable propositions is an important structure in constructive topology and real analysis, as it represents the set of open propositions in synthetic topology (Bidlingmaier, Faissole & Spitters 2019) and is used to construct a distinct and smaller version of the Dedekind real numbers (Univalent Foundations Project 2013, Bidlingmaier, Faissole & Spitters 2019) that is not provably equivalent to either the usual Dedekind real numbers or the Cauchy real numbers in the absence of excluded middle or countable choice. In addition, positivity (i.e. $0 \lt x$) of the HoTT book real numbers is quasidecidable (Gilbert 2017).

The set of quasidecidable propositions is also used for the dominance in synthetic domain theory, such as in the effective topos (Sterling & Ye 2025), where by countable choice it coincides with the set of semidecidable propositions and is thus called the Rosolini dominance. However, unlike the set of semidecidable propositions, even in the absence of countable choice, the set of quasidecidable propositions is always an $\mathbb{N}$-overt dominance (Bidlingmaier, Faissole & Spitters 2019, Escardo 2020).

Definition

Definition

The set of Sierpiński semidecidable truth values or set of quasidecidable truth values $\Sigma$ is defined in the following equivalent ways:

• as the initial $\sigma$-frame
• as the $\omega$-cpo completion of the partial order of the boolean domain, see Bidlingmaier, Faissole, & Spitters 2019
• as the pointed $\omega$-cpo completion of the set with one element (Bidlingmaier, Faissole, & Spitters 2019), or equivalently the partial map classifier of the set with one element, for the definition of the partial map classifier given in Altinkirch, Danielsson, & Kraus 2016
• impredicatively as the smallest subset of the set of truth values $\Omega$ closed under truth, falsehood, and existential quantification over the natural numbers, see Escardo 2020.

The set of quasidecidable truth values is also called Sierpiński space (Altinkirch, Danielsson, & Kraus 2016, Gilbert 2017, Bidlingmaier, Faissole, & Spitters 2019) or the Sierpiński type (de Jong, Kraus, Mohammadzadeh, & Forsberg 2026).

Comment: since the set of Sierpiński semi-decidable truth values always forms a dominance, perhaps it can be called the Sierpinski dominance, though this term is not yet used in the literature. The term Sierpiński space is overloaded since it is more commonly used to refer to the topological space of the set of truth values equipped with the Scott topology, and the term Sierpiński type has type theoretic connotations that are not appropriate in set theory based foundations.

Definition

A Sierpiński semidecidable proposition or quasidecidable proposition is a proposition $P$ such that there exist an element $p \in \Sigma$ such that $P$ holds if and only if $p = \top$, where $\top$ is the top of $\Sigma$.

$$\mathrm{isQuasiDecidable}(P) \coloneqq \exists p \in \Sigma.P \iff p = \top$$

The set of quasidecidable truth values $\Sigma$ sits in a hierarchy of subsets of the set of truth values:

$$\mathbb{2} \subseteq \Sigma^0_1 \subseteq \Sigma \subseteq \Omega$$

where $\mathbb{2}$ is the boolean domain, $\Sigma^0_1$ is the set of semi-decidable truth values of the usual notion, and $\Omega$ is the set of all truth values.

Constructive taboos

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

Rosolini dominance

In classical mathematics and in constructive mathematics which accepts countable choice, the set of quasidecidable propositions is equivalent to the set of semidecidable propositions (Sterling & Ye 2025, de Jong, Kraus, Mohammadzadeh, & Forsberg 2026), and is thus called the Rosolini 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) and is equivalent to a form of choice called Rosolini propositional choice (Escardo & Knapp 2017) or Escardo-Knapp choice (de Jong, Kraus, Mohammadzadeh, & Forsberg 2026), which in turn ins equivalent to the statement that every quasidecidable proposition is semidecidable.

LPO and Phoa’s principle

In classical mathematics, and in constructive mathematics which accept the limited principle of omniscience (LPO), the set of quasidecidable 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 quasidecidable 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 quasidecidable propositions, this implies that the boolean domain coincide with the set of quasidecidable propositions by definition of the set of quasidecidable propositions.

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

This result also implies that every semidecidable proposition is a decidable proposition if and only if LPO holds, since the set of semidecidable propositions is a superset of the booleans and a subset of the set of quasidecidable propositions.

On the other hand, in synthetic topology and synthetic domain theory, one sometimes sees Phoa's principle or synthetic quasi-coherence assumed for the $\mathbb{N}$-overt dominance, in order to emulate the behavior of Sierpinski space, where every function is monotonic. Since the set of quasidecidable propositions is an $\mathbb{N}$-overt dominance, it is consistent to assume such axioms for the set of quasidecidable propositions, such as Phoa's principle for the set of quasidecidable propositions in the effective topos. However, such axioms are inconsistent with LPO:

Theorem

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

Proof

LPO is equivalent to the fact that the boolean domain coincides with the set of quasidecidable 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 quasidecidable 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 quasidecidable 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 quasidecidable propositions $\Sigma$ implies Phoa's principle for $\Sigma$, and so is thus inconsistent with LPO.

Related concepts

• decidable proposition

• proposition, truth value

• semidecidable proposition

• synthetic topology, synthetic domain theory

• dominance

• $\sigma$-frame

• effective topos

References

• 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]

• Martin Escardo. Quasidecidable propositions. Agda code with comments, 2020. (URL).

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

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• Thorsten Altenkirch, Nils A. Danielsson, Nicolai Kraus, Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type, FoSSaCS 2017, Lecture Notes in Computer Science 10203 Springer (2017) [doi:10.1007/978-3-662-54458-7_31, arXiv:1610.09254]

• Gaëtan Gilbert. Formalising real numbers in homotopy type theory. In CPP’17, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pages 112–124, 2017. [doi:10.1145/3018610.3018614].

• Martin E. Bidlingmaier, Florian Faissole, Bas Spitters, Synthetic topology in Homotopy Type Theory for probabilistic programming. Mathematical Structures in Computer Science, 2021;31(10):1301-1329. [doi:10.1017/S0960129521000165, arXiv:1912.07339]

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

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