Namespaces
Variants
Actions

Difference between revisions of "Decidable formula"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX, Refs, MSC (please check MSC))
 
Line 1: Line 1:
''(in a given system)''
+
{{MSC|03B25}}
 +
{{TEX|done}}
  
A formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030370/d0303701.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030370/d0303702.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030370/d0303703.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030370/d0303704.png" /> 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.)
+
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 "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|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 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" .
+
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====  
====Comments====
+
{|
A formula that is not decidable in a system is called an undecidable formula in this system, cf. also [[Undecidability|Undecidability]].
+
|-
 
+
|valign="top"|{{Ref|Ra}}||valign="top"| M.O. Rabin, "Decidable theories" J. Barwise (ed.), ''Handbook of mathematical logic'', North-Holland (1977) pp. 595–629
====References====
+
|-
<table><TR><TD valign="top">[a1]</TD> <TD valign="top"M.O. Rabin,   "Decidable theories" J. Barwise (ed.) , ''Handbook of mathematical logic'' , North-Holland (1977) pp. 595–629</TD></TR></table>
+
|}

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
How to Cite This Entry:
Decidable formula. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Decidable_formula&oldid=18866
This article was adapted from an original article by V.E. Plisko (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article