Semidecidable Propositions

Definition

A proposition $P$ is semidecidable if there is an effective procedure that eventually confirms $P$ when $P$ is true, but may run forever when $P$ is false.

Equivalently, semidecidability means that truth of $P$ can be recognized by computation, even if falsity need not be decidable. Thus semidecidability is weaker than decidability.

Remarks

In computability theory, semidecidable predicates correspond to recursively enumerable or recognizable sets.

In type theory, semidecidable propositions are used to classify domains of definition for the semidecidable lifting monad in partiality in type theory.

Related Concepts

Decidable
Lifting Monad
Partiality (Type Theory)
Recursively Enumerable Language