A property that describes a set or decision problem $S$ for which there exists a decision procedure that will always deliver the right answer, if it delivers an answer at all, but may deliver no answer if $a$ is not in $S$. As an example, the set of theorems of Peano Arithmetic is semidecidable; for every theorem $\phi$ of $\text{PA}$, a proof verifying $\phi$ is guaranteed to appear in a finite amount of time by searching through an enumeration of proofs. On the other hand, if $\psi$ is not proven by $\text{PA}$, this procedure may never halt.