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, Gilbert 2017, 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. Unlike the Rosolini dominance, the set of quasidecidable truth values is always a dominance.

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 propositional choice

In classical mathematics and in constructive mathematics which accepts countable choice, the set of quasidecidable propositions is just 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 $\mathbb{N}$-overt is equivalent to a form of choice called Rosolini propositional choice (Escardo & Knapp 2017) or Escardo-Knapp choice (de Jong, Kraus, Mohammadzadeh, & Forsberg 2026), see section 2.8 of Escardo & Knapp 2017 for more details.

LPO and Phoa’s principle

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

Theorem

The limited principle of omniscience holds if and only if the set of quasidecidable propositions coincides with the boolean domain.

Proof

The limited principle of omniscience 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 the limited principle of omniscience.

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. However, such axioms are inconsistent with the limited principle of omniscience:

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, dominance

• $\sigma$-frame

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 Anders Danielsson, Nicolai Kraus, Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (abs: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]