Let (N, <) be the model with universe N and the "less than" relation. Show that Th(N, <) is decidable.
Reduce Th(AJ, <) to Th(fV, +), which we've already shown to be decidable. To do so, show how to convert a sentence 0, over the language of Th(A(, <), to a sentence 02 over the language of Th(AF, +) while preserving truth or falsity in the respective models. Replace every occurrence of i < j in X1 by the formula
]k [ (i+k j) A (k+kok) ] in 02, where k is a different new variable each time. Sentence P2 is equivalent to X1 because "i is less than j" means that we can add a nonzero value to i and obtain j. Putting 02 into prenex-normal form, as required by the algorithm for deciding Th(JV, +), requires a bit of additional work. The new existential quantifiers are brought to the front of the sentence. To do so, these quantifiers must pass through Boolean operations that appear in the sentence. Quantifiers can be brought through the operations of A and V without change. Passing through - changes 3 to V and vice-versa. Thus -3k 0 becomes the equivalent expression Vk -'y, and -Vk V) becomes 3k -'f .
A logical system or theory is decidable if the set of all well-formed formulas valid in the system is decidable. That is, there exists an algorithm such that for every formula in the system the algorithm is capable of deciding in finitely many steps whether the formula is valid in the system or not.
Example: Propositional logic is decidable, because there exists for it an algorithm?truth-table construction?such that for every formula which combines M atomic formulas there is a maximum number N = 2^M of steps such that after completing those N steps ...
Decidable systems are investigated.