Topic summary
Semidecidability
Extracted from the Wikipedia article Decidability (logic).
Semidecidability
A property of a theory or logical system weaker than decidability is semidecidability. A theory is semidecidable if there is a well-defined method whose result, given an arbitrary formula, arrives as positive, if the formula is in the theory; otherwise, may never arrive at all or arrives as negative. Equivalently, a logical system is semidecidable if there is a well-defined method for generating a sequence of theorems such that each theorem will eventually be generated. This is different from decidability because in a semidecidable system there may be no effective procedure for checking that a formula is not a theorem.