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 set of all semi-decidable propositions is typically called the **Rosolini dominance**, though it may not be a dominance without certain assumptions such as countable choice or excluded middle.

If the foundations of mathematics has the Cauchy real numbers $\mathbb{R}_C$ as well, then $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$

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

- Andrej Bauer, Davorin Lešnik,
*Metric Spaces in Synthetic Topology*, 2010 (pdf)

Last revised on January 27, 2024 at 18:07:40. See the history of this page for a list of all contributions to it.