Representability in $\Th{Q}$source

Representability of a numerical function in Q

A function $f(x_0,\ldots,x_k)$source from the natural numbers to the natural numbers is said to be em representable in $\Th{Q}$source if there is a formula $!A_f(x_0,\dots,x_k,y)$source such that whenever $f(n_0,\dots,n_k) = m$source, $\Th{Q}$source proves

1. $!A_f(\num{n_0}, \dots, \num{n_k}, \num{m})$source

2. $\lforall[y][(!A_f(\num{n_0}, \dots, \num{n_k}, y) \lif \num{m} = y)]$source.

Functions representable in Q are exactly the computable functions

A function is representable in $\Th{Q}$source if and only if it is computable.

Provable instances of a representing formula identify the correct value

If $f(x_0, \dots, x_k)$source is representable in $\Th{Q}$source, there is a formula $!A(x_0, \dots, x_k, y)$source such that

Proof

The “if” part is the definition of function representability in Qits first clause, proving the correct numeral instance. The “only if” part is seen as follows: Suppose $\Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{m})$source but $m \neq f(n_0, \dots, n_k)$source. Let $l = f(n_0, \dots, n_k)$source. By the definition of function representability in Qits first clause, proving the correct numeral instance, $\Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{l})$source. By the definition of function representability in Qits second clause, proving uniqueness of the output, $\lforall[y][(!A_f(\num{n_0}, \dots, \num{n_k}, y) \lif \num{l} = y)]$source. Using logic and the assumption that $\Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{m})$source, we get that $\Th{Q} \Proves \eq[\num{l}][\num{m}]$source. On the other hand, by the lemma that Q proves distinct numerals unequal, $\Th{Q} \Proves \eq/[\num{l}][\num{m}]$source. So $\Th{Q}$source is inconsistent. But that is impossible, since $\Th{Q}$source is satisfied by the standard model (see the definition of the standard model of arithmetic), $\Sat{N}{\Th{Q}}$source, and satisfiable theories are always consistent by the Soundness Theorem (references the soundness corollary that satisfiable theories are consistent, for axiomatic derivations, the soundness corollary that satisfiable theories are consistent, for sequent calculus, the soundness corollary that satisfiable theories are consistent, for natural deduction, and the soundness corollary that satisfiable theories are consistent, for tableaux).

Every function representable in Q is computable

Every function that is representable in $\Th{Q}$source is computable.

Proof

Let's first give the intuitive idea for why this is true. To compute $f$source, we do the following. List all the possible derivations $\delta$source in the language of arithmetic. This is possible to do mechanically. For each one, check if it is a derivation of a formula of the form $!A_f(\num{n_0}, \dots, \num{n_k}, \num{m})$source (the formula representing $f$source in $\Th{Q}$source from the lemma equating provable representing instances with correct function values). If it is, $m = f(n_0, \dots, n_k)$source by the lemma equating provable representing instances with correct function values, and we've found the value of $f$source. The search terminates because $\Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{f(n_0, \dots, n_k)})$source, so eventually we find a $\delta$source of the right sort.

This is not quite precise because our procedure operates on derivations and formulas instead of just on numbers, and we haven't explained exactly why “listing all possible derivations” is mechanically possible. But as we've seen, it is possible to code terms, formulas, and derivations by Gödel numbers. We've also introduced a precise model of computation, the general recursive functions. And we've seen that the relation $\Prf[\Th{Q}](d,y)$source, which holds iff $d$source is the Gödel number of a derivation of the formula with Gödel number $y$source from the axioms of $\Th{Q}$source, is (primitive) recursive. Other primitive recursive functions we'll need are $\fn{num}$source (the proposition that numeral coding is primitive recursive) and $\fn{Subst}$source (the proposition that substitution coding is primitive recursive). From these, it is possible to define $f$source by minimization; thus, $f$source is recursive.

First, define

This looks complicated, but it's just the function $A(n_0, \dots, n_k, m) = \Gn{!A_f(\num{n_0}, \dots, \num{n_k}, \num{m})}$source.

Now, consider the relation $R(n_0, \dots, n_k, s)$source which holds if $(s)_0$source is the Gödel number of a derivation from $\Th{Q}$source of $!A_f(\num{n_0}, \dots, \num{n_k}, \num{(s)_1})$source:

If we can find an $s$source such that $R(n_0, \dots, n_k, s)$source holds, we have found a pair of numbers---$(s)_0$source and $(s)_1$source---such that $(s)_0$source is the Gödel number of a derivation of $A_f(\num{n_0}, \dots, \num{n_k}, (s)_1)$source. So looking for $s$source is like looking for the pair $d$source and $m$source in the informal proof. And a computable function that “looks for” such an $s$source can be defined by regular minimization. Note that $R$source is regular: for every $n_0$source, dots, $n_k$source, there is a derivation $\delta$source of $\Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{f(n_0, \dots, n_k)})$source, so $R(n_0, \dots, n_k, s)$source holds for $s = \tuple{\Gn{\delta}, f(n_0, \dots, n_k)}$source. So, we can write $f$source as

The beta function lemma

There is a function $\beta(d,i)$source such that for every sequence $a_0$source, dots, $a_n$source there is a number $d$source, such that for every $i \le n$source, $\beta(d,i) = a_i$source. Moreover, $\beta$source can be defined from the basic functions using just composition and regular minimization.

Relatively prime natural numbers

Two natural numbers $a$source and $b$source are relatively prime iff their greatest common divisor is $1$source; in other words, they have no other divisors in common.

Congruence modulo a natural number

Natural numbers $a$source and $b$source are congruent modulo $c$source, $a \equiv b \mod c$source, iff $c \mid (a-b)$source, i.e., $a$source and $b$source have the same remainder when divided by $c$source.

Sunzi theorem on simultaneous congruences

Suppose $x_0$source, dots, $x_n$source are (pairwise) relatively prime. Let $y_0$source, dots, $y_n$source be any numbers. Then there is a number $z$source such that

Exercise defining order divisibility and remainder without primitive recursion

Show that the relations $x < y$source, $x \mid y$source, and the function $\fn{rem}(x,y)$source can be defined without primitive recursion. You may use $0$source, successor, plus, times, $\Char{=}$source, projections, and bounded minimization and quantification.

Simulation of primitive recursion by regular minimization

If $h$source can be defined from $f$source and $g$source using primitive recursion, it can be defined from $f$source, $g$source, the functions $\Zero$source, $\Succ$source, $\Proj{n}{i}$source, $\Add$source, $\Mult$source, $\Char{=}$source, using composition and regular minimization.

Proof

First, define an auxiliary function $\hat h(\vec x, y)$source which returns the least number $d$source such that $d$source codes a sequence which satisfies

1. $(d)_0 = f(\vec x)$source, and

2. for each $i < y$source, $(d)_{i+1} = g(\vec x, i, (d)_i)$source,

where now $(d)_i$source is short for $\beta(d,i)$source. In other words, $\hat h$source returns the sequence $\tuple{h(\vec x, 0), h(\vec x, 1), \dots, h(\vec x, y)}$source. We can write $\hat h$source as

Note: no primitive recursion is needed here, just minimization. The function we minimize is regular because of the beta function lemma the beta function lemma.

But now we have

so $h$source can be defined from the basic functions using just composition and regular minimization.

Representability of the zero function

The zero function $\Zero(x) = 0$source is represented in $\Th{Q}$source by $!A_{\Zero}(x,y) \ident \eq[y][\Obj 0]$source.

Representability of the successor function

The successor function $\Succ(x) = x+1$source is represented in $\Th{Q}$source by $!A_{\Succ}(x,y) \ident \eq[y][x']$source.

Representability of projection functions

The projection function $\Proj{n}{i}(x_0, \dots, x_{n-1}) = x_i$source is represented in $\Th{Q}$source by

Exercise proving representability of the three initial functions

Prove that $\eq[y][\Obj 0]$source, $\eq[y][x']$source, and $\eq[y][x_i]$source represent $\Zero$source, $\Succ$source, and $\Proj{n}{i}$source, respectively.

Representability of the characteristic function of equality

The characteristic function of $=$source,

is represented in $\Th{Q}$source by

Q proves inequality of distinct numerals

Given natural numbers $n$source and $m$source, if $n \neq m$source, then $\Th{Q} \Proves \eq/[\num n][\num m]$source.

Proof

Use induction on $n$source to show that for every $m$source, if $n \neq m$source, then $Q \Proves \eq/[\num n][\num m]$source.

In the base case, $n = 0$source. If $m$source is not equal to $0$source, then $m = k + 1$source for some natural number $k$source. We have an axiom that says $\lforall[x][\eq/[0][x']]$source. By a quantifier axiom, replacing $x$source by $\num k$source, we can conclude $\eq/[0][\num k']$source. But $\num k'$source is just $\num m$source.

In the induction step, we can assume the claim is true for $n$source, and consider $n+1$source. Let $m$source be any natural number. There are two possibilities: either $m = 0$source or for some $k$source we have $m = k+1$source. The first case is handled as above. In the second case, suppose $n+1 \neq k+1$source. Then $n \neq k$source. By the induction hypothesis for $n$source we have $\Th{Q} \Proves \eq/[\num n][\num k]$source. We have an axiom that says $\lforall[x][\lforall[y][\eq[x'][y'] \lif \eq[x][y]]]$source. Using a quantifier axiom, we have $\eq[\num n'][\num k'] \lif \eq[\num n][\num k]$source. Using propositional logic, we can conclude, in $\Th{Q}$source, $\eq/[\num n][\num k] \lif \eq/[\num n'][\num k']$source. Using modus ponens, we can conclude $\eq/[\num n'][\num k']$source, which is what we want, since $\num k'$source is $\num m$source.

Explain

Note that the lemma does not say much: in essence it says that $\Th{Q}$source can prove that different numerals denote different objects. For example, $\Th{Q}$source proves $0'' \neq 0'''$source. But showing that this holds in general requires some care. Note also that although we are using induction, it is induction outside of $\Th{Q}$source.

Proof

[Proof of the proposition representing the characteristic function of equality] If $n = m$source, then $\num{n}$source and $\num{m}$source are the same term, and $\Char{=}(n, m) = 1$source. But $\Th{Q} \Proves (\eq[\num{n}][\num{m}] \land \eq[\num{1}][\num{1}])$source, so it proves $!A_=(\num{n}, \num{m}, \num{1})$source. If $n \neq m$source, then $\Char=(n, m) = 0$source. By the lemma that Q proves distinct numerals unequal, $\Th{Q} \Proves \eq/[\num{n}][\num{m}]$source and so also $(\eq/[\num{n}][\num{m}] \land \Obj 0 = \Obj 0)$source. Thus $\Th{Q} \Proves !A_=(\num{n}, \num{m}, \num{0})$source.

For the second part, we also have two cases. If $n = m$source, we have to show that $\Th{Q} \Proves \lforall[y][(!A_=(\num{n}, \num{m}, y) \lif \eq[y][\num{1}])]$source. Arguing informally, suppose $!A_=(\num{n}, \num{m}, y)$source, i.e.,

The left disjunct implies $\eq[y][\num{1}]$source by logic; the right contradicts $\eq[\num{n}][\num{n}]$source which is provable by logic.

Suppose, on the other hand, that $n \neq m$source. Then $!A_=(\num{n}, \num{m}, y)$source is

Here, the left disjunct contradicts $\eq/[\num{n}][\num{m}]$source, which is provable in $\Th{Q}$source by the lemma that Q proves distinct numerals unequal; the right disjunct entails $\eq[y][\num{0}]$source.

Representability of addition

The addition function $\Add(x_0, x_1) = x_0+x_1$source is represented in $\Th{Q}$source by

Q computes each sum of numerals

$\Th{Q} \Proves \eq[(\num{n} + \num{m})][\num{n+m}]$source

Proof

We prove this by induction on $m$source. If $m = 0$source, the claim is that $\Th{Q} \Proves \eq[(\num{n} + \Obj 0)][\num{n}]$source. This follows by axiom $!Q_4$source. Now suppose the claim for $m$source; let's prove the claim for $m+1$source, i.e., prove that $\Th{Q} \Proves \eq[(\num{n} + \num{m+1})][\num{n+m+1}]$source. Note that $\num{m+1}$source is just $\num{m}'$source, and $\num{n+m+1}$source is just $\num{n+m}'$source. By axiom $!Q_5$source, $\Th{Q} \Proves \eq[(\num{n} + \num{m}')][(\num{n}+\num{m})']$source. By induction hypothesis, $\Th{Q} \Proves \eq[(\num{n} + \num{m})][\num{n+m}]$source. So $\Th{Q} \Proves \eq[(\num{n} + \num{m}')][\num{n+m}']$source.

Proof

[Proof of the proposition representing addition] The formula $!A_\Add(x_0, x_1, y)$source representing $\Add$source is $\eq[y][(x_0 + x_1)]$source. First we show that if $\Add(n, m) = k$source, then $\Th{Q} \Proves !A_\Add(\num{n}, \num{m}, \num{k})$source, i.e., $\Th{Q} \Proves \eq[\num{k}][(\num{n} + \num{m})]$source. But since $k = n + m$source, $\num{k}$source just is $\num{n+m}$source, and we've shown in the lemma that Q computes sums of numerals that $\Th{Q} \Proves \eq[(\num{n} + \num{m})][\num{n+m}]$source.

We also have to show that if $\Add(n, m) = k$source, then

Suppose we have $\eq[(\num{n} + \num{m})][y]$source. Since

we can replace the left side with $\num{n+m}$source and get $\eq[\num{n+m}][y]$source, for arbitrary $y$source.

Representability of multiplication

The multiplication function $\Mult(x_0, x_1) = x_0 \cdot x_1$source is represented in $\Th{Q}$source by

Proof

Exercise.

Q computes each product of numerals

$\Th{Q} \Proves \eq[(\num{n} \times \num{m})][\num{n \cdot m}]$source

Proof

Exercise.

Exercise proving the numeral multiplication lemma

Prove the lemma that Q computes products of numerals.

Exercise proving representability of multiplication

Use the lemma that Q computes products of numerals to prove the proposition representing multiplication.

Explain

Recall that we use $\times$source for the function symbol of the language of arithmetic, and $\cdot$source for the ordinary multiplication operation on numbers. So $\cdot$source can appear between expressions for numbers (such as in $m \cdot n$source) while $\times$source appears only between terms of the language of arithmetic (such as in $(\num{m} \times \num{n})$source). Even more confusingly, $+$source is used for both the function symbol and the addition operation. When it appears between terms---e.g., in $(\num{n} + \num{m})$source---it is the $2$source-place function symbol of the language of arithmetic, and when it appears between numbers---e.g., in $n+m$source---it is the addition operation. This includes the case $\num{n+m}$source: this is the standard numeral corresponding to the number $n+m$source.