more from this thinker | more from this text
Full Idea
A set of expressions is 'decidable' iff there exists an effective procedure (qv) that, given some expression, will decide whether or not the expression is included in the set (i.e. doesn't contradict it).
Gist of Idea
Expressions are 'decidable' if inclusion in them (or not) can be proved
Source
Herbert B. Enderton (A Mathematical Introduction to Logic (2nd) [2001], 1.7)
Book Ref
Enderton,Herbert B.: 'A Mathematical Introduction to Logic' [Academic Press 2001], p.62
A Reaction
This is obviously a highly desirable feature for a really reliable system of expressions to possess. All finite sets are decidable, but some infinite sets are not.
| 18758 | Validity is provable, but invalidity isn't, because the model is infinite [Church, by McGee] |
| 9996 | Expressions are 'decidable' if inclusion in them (or not) can be proved [Enderton] |
| 10080 | 'Effective' means simple, unintuitive, independent, controlled, dumb, and terminating [Smith,P] |
| 10087 | A theory is 'decidable' if all of its sentences could be mechanically proved [Smith,P] |
| 10088 | Any consistent, axiomatized, negation-complete formal theory is decidable [Smith,P] |
| 10156 | 'Recursion theory' concerns what can be solved by computing machines [Feferman/Feferman] |
| 10155 | Both Principia Mathematica and Peano Arithmetic are undecidable [Feferman/Feferman] |