Decidability (logic)
Encyclopedia
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. 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 formulas 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
.
s or in terms of computable function
s. 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.).
, 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 (provided the finitely axiomatizable theory Robinson Arithmetic is consistent; this proviso is implicit in every undecidability claim made in this article). 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 sequent
s, or the consequence relation {(Г, A) | Г ⊧ A} of the logic.
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 field
s, 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 which 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 which includes or interprets Robinson arithmetic is also (essentially) undecidable.
Methods used to establish decidability include quantifier elimination
, model completeness, and Vaught's test.
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.
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.
. For example, the theory of algebraically closed field
s 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
.
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, the term decidable refers to the decision problem
Decision problem
In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...
, the question of the existence of an effective method
Effective method
In computability theory, an effective method is a procedure that reduces the solution of some class of problems to a series of rote steps which, if followed to the letter, and as far as may be necessary, is bound to:...
for determining membership in a set of formulas. 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
Theory (mathematical logic)
In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...
(set of formulas 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
Undecidable problem
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is impossible to construct a single algorithm that always leads to a correct yes-or-no answer....
.
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 methodEffective method
In computability theory, an effective method is a procedure that reduces the solution of some class of problems to a series of rote steps which, if followed to the letter, and as far as may be necessary, is bound to:...
s or in terms of computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
s. 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 componentSyntax (logic)
In logic, syntax is anything having to do with formal languages or formal systems without regard to any interpretation or meaning given to them...
, which among other things determines the notion of provability
Formal proof
A formal proof or derivation is a finite sequence of sentences each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system...
, 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
Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
establishes the equivalence of semantic and syntactic consequence. In other settings, such as linear logic
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
, 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
Truth table
A truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—to compute the functional values of logical expressions on each of their functional arguments, that is, on each combination of values taken by their...
method can be used to determine whether an arbitrary propositional formula
Propositional formula
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value...
is logically valid.
First-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
is not decidable in general; in particular, the set of logical validities in any signature
Signature (logic)
In logic, especially mathematical logic, a signature lists and describes the non-logical symbols of a formal language. In universal algebra, a signature lists the operations that characterize an algebraic structure. In model theory, signatures are used for both purposes.Signatures play the same...
that includes equality and at least one other predicate with two or more arguments is not decidable (provided the finitely axiomatizable theory Robinson Arithmetic is consistent; this proviso is implicit in every undecidability claim made in this article). Logical systems extending first-order logic, such as second-order logic
Second-order logic
In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory....
and type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, are also undecidable.
The validities of monadic predicate calculus
Monadic predicate calculus
In logic, the monadic predicate calculus is the fragment of predicate calculus in which all predicate letters are monadic , and there are no function letters...
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
Ternary logic
In logic, a three-valued logic is any of several many-valued logic systems in which there are three truth values indicating true, false and some indeterminate third value...
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 sequent
Sequent
In proof theory, a sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. In the sequent calculus, the name sequent is used for the construct which can be regarded as a specific kind of judgment, characteristic to this deduction system.-...
s, or the consequence relation {(Г, A) | Г ⊧ A} of the logic.
Decidability of a theory
A theoryTheory (mathematical logic)
In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...
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 field
Real closed field
In mathematics, a real closed field is a field F that has the same first-order properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers.-Definitions:...
s, and Presburger arithmetic
Presburger arithmetic
Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely...
, while the theory of groups
Group (mathematics)
In mathematics, a group is an algebraic structure consisting of a set together with an operation that combines any two of its elements to form a third element. To qualify as a group, the set and the operation must satisfy a few conditions called group axioms, namely closure, associativity, identity...
and Robinson arithmetic
Robinson arithmetic
In mathematics, Robinson arithmetic, or Q, is a finitely axiomatized fragment of Peano arithmetic , first set out in R. M. Robinson . Q is essentially PA without the axiom schema of induction. Since Q is weaker than PA, it is incomplete...
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
Complete theory
In mathematical logic, a theory is complete if it is a maximal consistent set of sentences, i.e., if it is consistent, and none of its proper extensions is consistent...
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 which 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
Robinson arithmetic
In mathematics, Robinson arithmetic, or Q, is a finitely axiomatized fragment of Peano arithmetic , first set out in R. M. Robinson . Q is essentially PA without the axiom schema of induction. Since Q is weaker than PA, it is incomplete...
is known to be essentially undecidable, and thus every consistent theory which includes or interprets Robinson arithmetic is also (essentially) undecidable.
Some decidable theories
Some decidable theories include (Monk 1976, p. 234):- The set of first-order logical validities in the signature with only equality, established by Leopold LöwenheimLeopold LöwenheimLeopold Löwenheim was a German mathematician, known for his work in mathematical logic. The Nazi regime forced him to retire because under the Nuremberg Laws he was considered only three quarters Aryan. In 1943 much of his work was destroyed during a bombing raid on Berlin...
in 1915. - The set of first-order logical validities in a signature with equality and one unary function, established by Ehrenfeucht in 1959.
- The first-order theory of the integers in the signature with equality and addition, also called Presburger arithmeticPresburger arithmeticPresburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely...
. The completeness was established by Mojżesz PresburgerMojzesz PresburgerMojżesz Presburger was a Polish Jewish mathematician, logician, and philosopher. He was a student of Alfred Tarski and is known for, among other things, having invented Presburger arithmetic as a student in 1929....
in 1929. - The first-order theory of Boolean algebras, established by Alfred TarskiAlfred TarskiAlfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
in 1949. - The first-order theory of algebraically closed fields of a given characteristic, established by Tarski in 1949.
- The first-order theory of real-closed ordered fields, established by Tarski in 1949.
- The first-order theory of Euclidean geometry, established by Tarski in 1949.
- The first-order theory of hyperbolic geometry, established by Schwabhäuser in 1959.
- Specific decidable sublanguages of set theoryDecidable sublanguages of set theoryIn mathematical logic, various sublanguages of set theory are decidable. These include:* Sets with Monotone, Additive, and Multiplicative Functions.* Sets with restricted quantifiers....
investigated in the 1980s through today.(Cantone et al., 2001)
Methods used to establish decidability include quantifier elimination
Quantifier elimination
Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. One way of classifying formulas is by the amount of quantification...
, 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 TrakhtenbrotBoris TrakhtenbrotBoris Avraamovich Trakhtenbrot or Boaz Trakhtenbrot is an Israeli and Russian mathematician in mathematical logic, algorithms, theory of computation and cybernetics. He worked at Akademgorodok, Novosibirsk during the 1960s and 1970s...
in 1953. - The first-order theory of the natural numbers with addition, multiplication, and equality, established by Tarski and Andrzej MostowskiAndrzej MostowskiAndrzej Mostowski was a Polish mathematician. He is perhaps best remembered for the Mostowski collapse lemma....
in 1949. - The first-order theory of the rational numbers with addition, multiplication, and equality, established by Julia RobinsonJulia RobinsonJulia Hall Bowman Robinson was an American mathematician best known for her work on decision problems and Hilbert's Tenth Problem.-Background and education:...
in 1949. - The first-order theory of groups, established by Mal'cev in 1961. 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.
- Peano arithmetic is essentially undecidable. Gödel's incompleteness theoremsGödel's incompleteness theoremsGödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
show that many other sufficiently strong theories of arithmetic share this property.
The interpretability
Interpretability
In mathematical logic, interpretability is a relation between formal theories that expresses the possibility of interpreting or translating one into the other.-Informal definition:Assume T and S are formal theories...
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
Many-one reduction
In computability theory and computational complexity theory, a many-one reduction is a reduction which converts instances of one decision problem into instances of a second decision problem. Reductions are thus used to measure the relative computational difficulty of two problems.Many-one...
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
Recursively enumerable set
In computability theory, traditionally called recursion theory, a set S of natural numbers is called recursively enumerable, computably enumerable, semidecidable, provable or Turing-recognizable if:...
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 completenessComplete theory
In mathematical logic, a theory is complete if it is a maximal consistent set of sentences, i.e., if it is consistent, and none of its proper extensions is consistent...
. For example, the theory of algebraically closed field
Algebraically closed field
In mathematics, a field F is said to be algebraically closed if every polynomial with one variable of degree at least 1, with coefficients in F, has a root in F.-Examples:...
s 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
Independence (mathematical logic)
In mathematical logic, independence refers to the unprovability of a sentence from other sentences.A sentence σ is independent of a given first-order theory T if T neither proves nor refutes σ; that is, it is impossible to prove σ from T, and it is also impossible to prove from T that...
.
See also
- László KalmárLászló KalmárLászló Kalmár was a Hungarian mathematician and Professor at the University of Szeged. Kalmár is considered the founder of mathematical logic and theoretical Computer Science in Hungary.- Biography :...
(1936) - Alonzo ChurchAlonzo ChurchAlonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...
(1956) - W.V.O. Quine (1953)
- MeyerMeyer- Companies :* Meyer Corporation* Fred Meyer, Inc., American hypermarket chain; currently a subsidiary of Kroger* Meyer Sound Laboratories- Places :* Meyer Township, Michigan* Meyer, Illinois, unincorporated community in Adams County, Illinois, USA...
and LambertLambert-Airports:*Lambert Field Airport, a private airport in Albany, Oregon, United States*Lambert-St. Louis International Airport, the primary airport for St...
(1967)