Section 3.0: Number Theory
This chapter focuses on the language of the number theory, i.e. the theory of the structure , as well as its reducts, i.e. , , , and .
The questions for each theory to ask are as follows.
- Is the theory decidable? Does it have a nice or finite set of axioms?
- What subsets are definable?
- What non-standard models are there for the theory?
An interesting thing about the number theory is that it contains a certain undecidable subtheory, implying that any theory that is at least as strong as this subtheory must be undecidable as well.
We want to compare the concepts of truth and proof; that is, we want to compare the set of sentences true in with the set of sentences that might be provable from an appropriate set of axioms.
Let , called the Gödel number of , be a unique number assigned to each wff of the language. Similarly, to each finite sequence of wffs (such as a deduction) we can assign a unique integer . There are three approaches now: self-reference, diagonalization, and computability approaches.
Let such that is definable in . Then, there is a sentence true in that is not deducible from .
We want a sentence that would say something like “I am not deducible from .” Note, that such a sentence just ought to be true in , and, hence, not deducible from . To do this, we need a way in which a sentence can self-reference itself. We can do this by creating another formula (free in ), determining its Gödel number , and substituting for in to obtain . The formula itself should say something like “If you substitute for in formula number , then it is not deducible in .” Then, will say “If you substitute for in formula number , then the resulting formula is not deducible from .” In other words, will say “ is not deducible from .”
First, we define a relation such that iff formula ( ) is deducible from using the deduction number ( where is the deduction). One can argue that, since is definable, so is (the proof of this is left for later subsections). Then, if defines , let where . What under assignment says is that is not definable from . Let . Then says that is not definable from .
- Corollary: is not definable in . Indeed, the theorem implies that if is definable, then there is .
- The Church’s thesis, being studied later, says that if a subset of is decidable, then it is definable in . Hence, is not decidable, and is not axiomatizable.
Consider a relation such that iff “ is true of ”: there is a wff such that , is the only free variable in , and is true in . Then is definable in iff for some , . Consider . Then, is not definable in . It can be shown that the only way can be not definable in , if “true in ” is not definable.
is not definable in (same as in the corollary above). is undecidable and not axiomatizable.
From Section 2.6 it follows, that if is effectively enumerable, then is effectively enumerable as well. Using, again, Church’s thesis, it will be shown later that is not effectively enumerable.
For an effectively enumerable set , .