World Library  
Flag as Inappropriate
Email this Article

Decidability (logic)

Article Id: WHEBN0000913118
Reproduction Date:

Title: Decidability (logic)  
Author: World Heritage Encyclopedia
Language: English
Subject: Alfred Tarski, Decision problem, Presburger arithmetic, Satisfiability, General set theory
Collection: Concepts in Logic, Metalogic, Proof Theory
Publisher: World Heritage Encyclopedia
Publication
Date:
 

Decidability (logic)

In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas, or, more precisely, an algorithm that can and will return a Boolean true or false value (instead of looping indefinitely). Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas (or theorems) can be effectively determined. A theory (set of sentences closed under logical consequence) in a fixed logical system is decidable if there is an effective method for determining whether arbitrary formulas are included in the theory. Many important problems are undecidable, that is, it has been proven that no effective method can exist for them.

Contents

  • Relationship to computability 1
  • Decidability of a logical system 2
  • Decidability of a theory 3
  • Some decidable theories 4
  • Some undecidable theories 5
  • Semidecidability 6
  • Relationship with completeness 7
  • See also 8
  • References 9
    • Notes 9.1
    • Bibliography 9.2

Relationship to computability

As with the concept of a decidable set, the definition of a decidable theory or logical system can be given either in terms of effective methods or in terms of computable functions. These are generally considered equivalent per Church's thesis. Indeed, the proof that a logical system or theory is undecidable will use the formal definition of computability to show that an appropriate set is not a decidable set, and then invoke Church's thesis to show that the theory or logical system is not decidable by any effective method (Enderton 2001, pp. 206ff.).

Decidability of a logical system

Each logical system comes with both a syntactic component, which among other things determines the notion of provability, and a semantic component, which determines the notion of logical validity. The logically valid formulas of a system are sometimes called the theorems of the system, especially in the context of first-order logic where Gödel's completeness theorem establishes the equivalence of semantic and syntactic consequence. In other settings, such as linear logic, the syntactic consequence (provability) relation may be used to define the theorems of a system.

A logical system is decidable if there is an effective method for determining whether arbitrary formulas are theorems of the logical system. For example, propositional logic is decidable, because the truth-table method can be used to determine whether an arbitrary propositional formula is logically valid.

First-order logic is not decidable in general; in particular, the set of logical validities in any signature that includes equality and at least one other predicate with two or more arguments is not decidable.[1] Logical systems extending first-order logic, such as second-order logic and type theory, are also undecidable.

The validities of monadic predicate calculus with identity are decidable, however. This system is first-order logic restricted to signatures that have no function symbols and whose relation symbols other than equality never take more than one argument.

Some logical systems are not adequately represented by the set of theorems alone. (For example, Kleene's logic has no theorems at all.) In such cases, alternative definitions of decidability of a logical system are often used, which ask for an effective method for determining something more general than just validity of formulas; for instance, validity of sequents, or the consequence relation {(Г, A) | Г ⊧ A} of the logic.

Decidability of a theory

A theory is a set of formulas, which here is assumed to be closed under logical consequence. The question of decidability for a theory is whether there is an effective procedure that, given an arbitrary formula in the signature of the theory, decides whether the formula is a member of the theory or not. This problem arises naturally when a theory is defined as the set of logical consequences of a fixed set of axioms. Examples of decidable first-order theories include the theory of real closed fields, and Presburger arithmetic, while the theory of groups and Robinson arithmetic are examples of undecidable theories.

There are several basic results about decidability of theories. Every inconsistent theory is decidable, as every formula in the signature of the theory will be a logical consequence of, and thus member of, the theory. Every complete recursively enumerable first-order theory is decidable. An extension of a decidable theory may not be decidable. For example, there are undecidable theories in propositional logic, although the set of validities (the smallest theory) is decidable.

A consistent theory that has the property that every consistent extension is undecidable is said to be essentially undecidable. In fact, every consistent extension will be essentially undecidable. The theory of fields is undecidable but not essentially undecidable. Robinson arithmetic is known to be essentially undecidable, and thus every consistent theory that includes or interprets Robinson arithmetic is also (essentially) undecidable.

Some decidable theories

Some decidable theories include (Monk 1976, p. 234):

Methods used to establish decidability include quantifier elimination, model completeness, and Vaught's test.

Some undecidable theories

Some undecidable theories include (Monk 1976, p. 279):

  • The set of logical validities in any first-order signature with equality and either: a relation symbol of arity no less than 2, or two unary function symbols, or one function symbol of arity no less than 2, established by Trakhtenbrot in 1953.
  • The first-order theory of the natural numbers with addition, multiplication, and equality, established by Tarski and Andrzej Mostowski in 1949.
  • The first-order theory of the rational numbers with addition, multiplication, and equality, established by Julia Robinson in 1949.
  • The first-order theory of groups, established by Alfred Tarski in 1953.[2] Remarkably, not only the general theory of groups is undecidable, but also several more specific theories, for example (as established by Mal'cev 1961) the theory of finite groups. Mal'cev also established that the theory of semigroups and the theory of rings are undecidable. Robinson established in 1949 that the theory of fields is undecidable.
  • Robinson arithmetic (and therefore any consistent extension, such as Peano arithmetic) is essentially undecidable, as established by Raphael Robinson in 1950.

The interpretability method is often used to establish undecidability of theories. If an essentially undecidable theory T is interpretable in a consistent theory S, then S is also essentially undecidable. This is closely related to the concept of a many-one reduction in computability theory.

Semidecidability

A property of a theory or logical system weaker than decidability is semidecidability. A theory is semidecidable if there is an effective method which, given an arbitrary formula, will always tell correctly when the formula is in the theory, but may give either a negative answer or no answer at all when the formula is not in the theory. A logical system is semidecidable if there is an effective method for generating theorems (and only theorems) such that every 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.

Every decidable theory or logical system is semidecidable, but in general the converse is not true; a theory is decidable if and only if both it and its complement are semi-decidable. For example, the set of logical validities V of first-order logic is semi-decidable, but not decidable. In this case, it is because there is no effective method for determining for an arbitrary formula A whether A is not in V. Similarly, the set of logical consequences of any recursively enumerable set of first-order axioms is semidecidable. Many of the examples of undecidable first-order theories given above are of this form.

Relationship with completeness

Decidability should not be confused with completeness. For example, the theory of algebraically closed fields is decidable but incomplete, whereas the set of all true first-order statements about nonnegative integers in the language with + and × is complete but undecidable. Unfortunately, as a terminological ambiguity, the term "undecidable statement" is sometimes used as a synonym for independent statement.

See also

References

Notes

  1. ^ Trakhtenbrot, 1953
  2. ^ Tarski, A.; Mostovski, A.; Robinson, R. (1953), Undecidable Theories, Studies in Logic and the Foundation of Mathematics, North-Holland, Amsterdam 

Bibliography

  • Barwise, Jon (1982), "Introduction to first-order logic", in Barwise, Jon, Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland,  
  • Cantone, D., E. G. Omodeo and A. Policriti, "Set Theory for Computing. From Decision Procedures to Logic Programming with Sets," Monographs in Computer Science, Springer, 2001.
  • Chagrov, Alexander; Zakharyaschev, Michael (1997), Modal logic, Oxford Logic Guides 35, The Clarendon Press Oxford University Press,  
  •  
  • Enderton, Herbert (2001), A mathematical introduction to logic (2nd ed.), Boston, MA:  
  • Keisler, H. J. (1982), "Fundamentals of model theory", in Barwise, Jon, Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland,  
  • Monk, J. Donald (1976), Mathematical Logic, Berlin, New York:  
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
 
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
 
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.
 


Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.