nLab semi-decidable proposition



A proposition or truth value PP is semi-decidable or semidecidable if and only if there exists a sequence of booleans f2 f \in 2^\mathbb{N} such that PP if and only if there exists a natural number xx \in \mathbb{N} such that f(x)=1f(x) = 1.

isSemiDecidable(P)f2 .Px.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 C\mathbb{R}_C as well, then PP is semideciable if and only if there exists a Cauchy real number x Cx \in \mathbb{R}_C such that PP if and only if x>0x \gt 0.

isSemiDecidable(P)x C.Px>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 LPO \mathrm{LPO}_\mathbb{N} implies that every semi-decidable proposition is a decidable proposition.


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