Difference between revisions of "Decidable formula"
(Importing text file) |
(TeX, Refs, MSC (please check MSC)) |
||
| Line 1: | Line 1: | ||
| − | + | {{MSC|03B25}} | |
| + | {{TEX|done}} | ||
| − | A formula | + | A decidable formula is a formula $A$ of a given [[Formal system|formal system]] that is either provable in this system (that is, is a theorem) or refutable (that is, its negation $\neg A$ is provable). If every closed formula of a given formal system is decidable, then such a system is said to be complete. (Note that it is impossible to require that all, and not just the closed, formulas be decidable in the system. Thus, the formula $x=0$, where $x$ runs over natural numbers, expresses neither a true nor a false proposition and therefore neither it nor its negation is a theorem of formal arithmetic.) |
| − | The name | + | The name "decidable formula" comes from the fact that the truth or falsehood of the statement expressed by such a formula can be decided on the basis of the given system of axioms. By the [[Gödel incompleteness theorem]] there is an undecidable statement in any formal system of arithmetic, that is, a closed formula can be found that is not decidable in this system. In particular, the formula expressing the assertion that such a system is consistent turns out to be not decidable. |
| − | The term | + | The term "decidable formula" should be distinguished from the term "decidable predicate" . |
| + | ====Comments==== | ||
| + | A formula that is not decidable in a system is called an undecidable formula in this system, cf. also [[Undecidability]]. | ||
| − | + | ====References==== | |
| − | ==== | + | {| |
| − | + | |- | |
| − | + | |valign="top"|{{Ref|Ra}}||valign="top"| M.O. Rabin, "Decidable theories" J. Barwise (ed.), ''Handbook of mathematical logic'', North-Holland (1977) pp. 595–629 | |
| − | + | |- | |
| − | + | |} | |
Latest revision as of 22:25, 26 July 2012
2020 Mathematics Subject Classification: Primary: 03B25 [MSN][ZBL]
A decidable formula is a formula $A$ of a given formal system that is either provable in this system (that is, is a theorem) or refutable (that is, its negation $\neg A$ is provable). If every closed formula of a given formal system is decidable, then such a system is said to be complete. (Note that it is impossible to require that all, and not just the closed, formulas be decidable in the system. Thus, the formula $x=0$, where $x$ runs over natural numbers, expresses neither a true nor a false proposition and therefore neither it nor its negation is a theorem of formal arithmetic.)
The name "decidable formula" comes from the fact that the truth or falsehood of the statement expressed by such a formula can be decided on the basis of the given system of axioms. By the Gödel incompleteness theorem there is an undecidable statement in any formal system of arithmetic, that is, a closed formula can be found that is not decidable in this system. In particular, the formula expressing the assertion that such a system is consistent turns out to be not decidable.
The term "decidable formula" should be distinguished from the term "decidable predicate" .
Comments
A formula that is not decidable in a system is called an undecidable formula in this system, cf. also Undecidability.
References
| [Ra] | M.O. Rabin, "Decidable theories" J. Barwise (ed.), Handbook of mathematical logic, North-Holland (1977) pp. 595–629 |
Decidable formula. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Decidable_formula&oldid=27213