Editing Decidability (logic) (section)

==Decidability of a theory==

A [[theory (mathematical logic)|theory]] is a set of formulas, often assumed to be [[deductively closed|closed]] under [[logical consequence]]. Decidability for a theory concerns whether there is an effective procedure that decides whether the formula is a member of the theory or not, given an arbitrary formula in the signature of the theory. The problem of decidability arises naturally when a theory is defined as the set of logical consequences of a fixed set of axioms.

There are several basic results about decidability of theories. Every (non-[[Paraconsistent logic|paraconsistent]]) inconsistent theory is decidable, as every formula in the signature of the theory will be a logical consequence of, and thus a member of, the theory. Every [[complete theory|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.

Examples of decidable first-order theories include the theory of [[real closed field]]s, and [[Presburger arithmetic]], while the theory of [[group (mathematics)|groups]] and [[Robinson arithmetic]] are examples of undecidable theories.