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

Related concepts

• decidable proposition

• proposition, truth value

• synthetic topology, dominance

 References

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