CSC 341: April 20, 2007

From CSWiki

1 Instructor's notes for the class session
2 Study questions
- 2.1 Proposed Solutions

Instructor's notes for the class session

Theories and decidability

Mathematicians and mathematical logicians have developed completely formal notations for expressing propositions in various branches of mathematics, such as number theory. Some of these notations are more expressive than others.

Typically, in such a notation, there is a set of sentences, which is a subset of $Σ *$ . Some of the sentences express truths (in the intended model -- the collection of rules that assign meanings to the sentences); the set of true sentences is the theory of the notation (relative to that model).

Sipser considers two such theories: the theory of addition for natural numbers, $\textrm{Th}(\mathcal{N}, +)$ , and the theory of addition and multiplication for natural numbers, $\textrm{Th}(\mathcal{N}, +, \times)$ . In both theories, one gets Boolean operators and the usual variable-binding operators expressing universal and existential quantification; sentences are the well-formed expressions of the notation in which all of the variables are bound.

It turns out that $\textrm{Th}(\mathcal{N}, +)$ is decidable, while $\textrm{Th}(\mathcal{N}, +, \times)$ is not. The undecidability result is obtained by reduction from $A_\mathsf{TM}$ and depends on the fact that one can model the operation of a Turing machine in a sentence of $\textrm{Th}(\mathcal{N}, +, \times)$ . The details of the reduction are very messy, since this notation initially offers even fewer expressive resources than our notation for recursive function theory, but it turns out to be yet another model equivalent in power to the Turing-machine model.

Proving that $\textrm{Th}(\mathcal{N}, +)$ is decidable requires a more unusual approach. The idea is to begin by design a finite automaton for every atomic subformula of the sentence that we receive as input. Such an automaton accepts or rejects strings that express combinations of numerical values, expressed as bitstrings, for the variables that occur in the sentence, depending on whether the particular addition expressed by the atomic formula holds or fails to hold.

Next, we can apply the constructions used in chapter 1 to show that unions, intersections, and complements of regular languages are regular to construct similar automata for disjunctions, conjunctions, and negations of atomic subformulas.

One can get a finite automaton for an existentially quantified subformula from the finite automaton for its body by having it non-deterministically guess an appropriate bitstring for the value of the quantified variable and submit that bitstring, along with values for the other variables, to the finite automaton for the body. Finally, universal quantification can be reduced to negation and existential quantification.

Proceeding in this way, one eventually obtains a finite automaton for the original sentence, which has no free variables. Such an automaton accepts every input if the sentence is true and rejects every input if it is false. So we can simulate the operation of the automaton on any input, say $\varepsilon$ , accepting the original input sentence as true if the simulation accepts and rejecting it if the simulation rejects.

Sipser's construction presupposes that all of the quantifiers that occur in the sentence occur in one initial prefix of the sentence, with the rest of the sentence being the body of the last one. Not all sentences of $(\mathcal{N}, +)$ have this form, but it is not difficult to show that every sentence that does not have this form is equivalent to, and can be transformed algorithmically into, one that does.

This method won't work for $\textrm{Th}(\mathcal{N}, +, \times)$ . A finite automaton can determine whether a particular fact of addition is true, but not whether a particular fact of multiplication is true. More powerful automata can test multiplication facts, but either don't allow complementation (like pushdown automata) or sometimes fail to terminate (like Turing machines).

Since we can express negation in the notation for $\textrm{Th}(\mathcal{N}, +, \times)$ , the undecidability of this theory implies that it is not even Turing-recognizable: If it were Turing-recognizable, we could test for non-membership in the theory by testing for the membership of its negation ( $\varphi$ is false (i.e., a non-member of the theory) if, and only if, $\neg\varphi$ is true (i.e., a member of the theory). So if $\textrm{Th}(\mathcal{N}, +, \times)$ were Turing-recognizable, it would also be co-Turing-recognizable, so that, by Theorem 4.22, it would be decidable, which is impossible.

[edit]

The incompleteness of axiomatic systems for arithmetic

This shows that any finite set of axioms that we might propose as a basis for proving propositions in the theory of the addition and multiplication of natural numbers is bound to be either incomplete or inconsistent. For, given any finite set of axioms, we can build an enumerator that writes out every logical consequence of those axioms. So the set of provable sentences is Turing-recognizable. But the set of true sentences is not Turing-recognizable; so either there are some true sentences that are not provable or there are some provable sentences that are not true.

The logician Kurt Gödel first proved this proposition, for a very broad class of mathematical theories, in 1930. He showed how, given a theory in a sufficiently expressive notation and a set of axioms, one can construct a particular sentence of that notation that is true but not provable (if the axioms are consistent). Sipser does something similar in his proof of Theorem 6.17, although he uses the recursion theorem to make his construction very much simpler than Gödel's.

[edit]

Turing reducibility

We can generalize the notion of mapping reducibility to fit more closely our intuition that a language $A$ should be, in some sense, reducible to a language $B$ if having a decider for $B$ would enable use to design a Turing-machine decider for $A$ , by suitable preprocessing, postprocessing, and parallel processing. Indeed, the concept of Turing reducibility simply formalizes this intuition: Suppose we imagine the decider for $B$ as a black box, working in some way that we can't specify, and allow Turing machines to incorporate such black boxes into their construction. If there is a black-box-using Turing machine that decides $A$ , then we say that $A$ is Turing-reducible to $B$ . The black box is conventionally called an oracle for $B$ .

Turing-reducibility preserves undecidability, in the sense that, if $A$ is undecidable and is Turing-reducible to $B$ , then $B$ is undecidable.

The symbol $\le_{\mathrm{T}}$ is used to express this relation.

[edit]

Study questions

Express the statement "There is a natural number $n$ such that $n = 0$ " in the strict notation that Sipser specifies on page 225, using $R 1$ as the only relation symbol, and interpreting the notation with reference to the model $(\mathcal{N}, +)$ .
Express the statement "For every natural number $n$ , there is a natural number $m$ such that $n \le m$ }" in Sipser's notation, using $R 1$ as the only relation symbol, and interpreting the notation with reference to the model $(\mathcal{N}, +)$ .
Express the statement "There is a natural number $n$ such that $n = 1$ " in Sipser's notation, using $R 1$ as the only relation symbol, and interpreting the notation with reference to the model $(\mathcal{N}, +)$ .
Express the statement "For all natural numbers $n$ and $d$ , there are natural numbers $q$ and $r$ such that either $d = 0$ , or $r < d$ and $q \times d + r = n$ " in Sipser's notation, using $R 1$ and $R 2$ as the only relation symbols, and interpreting the notation with reference to the model $(\mathcal{N}, +, \times)$ .
Prove that Turing reducibility is transitive.

[edit]

Proposed Solutions

$\forall x \exists n [R_1(x,n,x)]$
$A \leq_{t} B$ and $B\leq_{t} C$ We can replace calls to oracle b for computation that calls to oracle c so all now we have are calls to oracle c.