nLab semi-decidable 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$$

The limited principle of omniscience for the natural numbers $\mathrm{LPO}_\mathbb{N}$ implies that every semi-decidable proposition is a decidable proposition.

In dependent type theory

In dependent type theory, the definition of semi-decidable makes sense for any type, not just the mere propositions. However, like many other definitions in dependent type theory, one has to make sure to use an equivalence of types instead of logical equivalence in the definition of a semi-decidable type; this ensures that, like for decidable types, all semi-decidable types are propositions.

Definition

A type $P$ is semi-decidable if there exists a sequence of booleans $f:\mathbb{N} \to \mathrm{bool}$ such that $P$ is equivalent to that there exists a natural number $x:\mathbb{N}$ such that $f(x) = 1$.

$$\mathrm{isSemiDecidable}(P) \coloneqq \left[\sum_{f:\mathbb{N} \to \mathrm{bool}} P \simeq \left[ \sum_{x:\mathbb{N}}f(x) =_{\mathrm{bool}} 1\right]\right]$$

where $[A]$ is the bracket type of the type $A$.

There is also a partially untruncated version of this, which is the type

$$\sum_{f:\mathbb{N} \to \mathrm{bool}} P \simeq \left[\sum_{x:\mathbb{N}}f(x) =_{\mathrm{bool}} 1\right]$$

of all boolean sequences $f$ for which $P$ is equivalent to there exists a natural number $x:\mathbb{N}$ such that $f(x) = 1$.

Set of semi-decidable truth values

The set of all semi-decidable truth values $\Sigma_0^1$ is defined as a subset of the set of truth values $\Omega$ containing all the semi-decidable truth values:

$$\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 truth values may not exist, so instead in order to construct the set of all semi-decidable truth values, we take any sub-$\sigma$-frame of truth values $\Sigma$ and collect the ones that are semi-decidable:

$$\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.

The set of all semi-decidable truth values is typically called the Rosolini dominance, though it is a dominance if and only if semi-decidable truth values are closed under existential quantification over the natural numbers, which follows from certain assumptions such as countable choice or excluded middle.

Relation to Cauchy real numbers

Let $\mathbb{R}_C$ denote the Cauchy real numbers. Then a proposition $P$ is semideciable if and only if there exists a Cauchy real number $x \in \mathbb{R}_C$ such that $P$ if and only if $x \gt 0$.

$$\mathrm{isSemiDecidable}(P) \coloneqq \exists x \in \mathbb{R}_C.P \iff x \gt 0$$

This implies that the Cauchy real numbers are an Archimedean ordered field admissible for the set of semi-decidable truth values $\Sigma_0^1$, and in fact that the Cauchy real numbers are the terminal Archimedean ordered field that is admissible for $\Sigma_0^1$.

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

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 quasi-decidable propositions (Escardo 2020) or Sierpiński semi-decidable propositions (de Jong, Kraus, Mohammadzadeh, & Forsberg 2026).

Definition

The set of Sierpiński semi-decidable truth values or set of quasi-decidable truth values $\Sigma$ is defined in the following equivalent ways:

• as the initial $\sigma$-frame
• as the partial map classifier of the set with one element, for the definition of the partial map classifier given in Altinkirch, Danielsson, & Kraus 2016
• as the free $\omega$-cpo on the boolean domain
• impredicatively as the intersection of all sub-$\sigma$-frames of the frame of truth values $\Omega$

Here a sub-$\sigma$-frame of $\Omega$ is one that is closed under existential quantifiers on the natural numbers.

The set of Sierpiński semi-decidable 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 semi-decidable proposition or quasi-decidable 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{isSierpinskiSemiDecidable}(P) \coloneqq \exists p \in \Sigma.P \iff p = \top$$

The set of Sierpiński semi-decidable 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.

The set of Sierpiński semi-decidable truth values is an important structure in constructive topology and real analysis, as it represents the set of open truth values 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 Sierpiński semi-decidable truth values is always a dominance.

In classical mathematics, and in constructive mathematics which accept the limited principle of omniscience, the set of Sierpiński semi-decidable truth values is just the boolean domain $\mathbb{2}$; in fact, that the boolean domain is the set of Sierpiński semi-decidable truth values is equivalent to the limited principle of omniscience. In classical mathematics and in constructive mathematics which accepts countable choice or the weak countable choice axiom $\mathrm{AC}_{\mathbb{N}, \mathbb{2}}$, the set of Sierpiński semi-decidable truth values is just the Rosolini dominance. The limited principle of omniscience also implies that the set of Sierpiński semi-decidable truth values is the Rosolini dominance since both are equivalent to the boolean domain under the assumption.

Related concepts

• decidable proposition

• proposition, truth value

• synthetic topology, dominance

• $\sigma$-frame

 References

• Andrej Bauer, Davorin Lešnik, Metric Spaces in Synthetic Topology, 2010 (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]

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