[FOM] 618: Adventures in Formalization 4

[Anthony Coulter]

On further consideration, I'm going to strengthen my argument from "the
first-order theory of the polynomially-computable reals is not decid-
able" to "there is no good way to even define a first-order theory of
the polynomially-computable reals."

How would one axiomatize such a theory? A number is polynomially-
computable iff there exists some an algorithm that produces a rational
approximation to the number which is accurate to within epsilon in a
number of steps of order O(f(-log(epsilon)). How do you express the
duration of a computation in logic? The usual way is to say, "There
exists a list of finite length, where each element in the list is drawn
from a countably infinite set (representing the machine states), the
first element of the list is a suitable "initial state," the last
element of the list represents a state that somehow encodes both (1)
the fact that the computation is complete, and (2) the result of that
computation, and each element in the list is linked to its successor
element by a "transition function" representing the machine's algorithm.

[This is, for example, how primitive recursive functions are imple-
mented in Peano arithmetic: We would rewrite the exponential equation
"10^4 = 1000" as "there exists a list of five numbers; the first
(zeroth) number is 1, the last (fourth) number is 10000, and each
number in the list is ten times its predecesor."]

If we attempt to do the same thing with the real numbers, we run into
two problems: First, the first-order theory of real numbers just isn't
complicated enough to build objects representing lists. (In Peano
arithmetic, you can do fancy number-theoretical tricks with the Chinese
Remainder Theorem to encode a finite list of numbers as a triplet of
integers, which can be further encoded as a single integer.) Second,
there's no way to quantify over transition functions. That is, when we
try to expand "there exists a computable number such that..." to "there
exists a list of machine states AND A COMPUTABLE FUNCTION linking each
item in the list to its successor such that..." we have problems axiom-
atizing the notion of a computable function---under what circumstances
does such a computable function exist? If we try to take the notion of
a function for granted, we aren't doing first-order logic anymore. So
the idea of a first-order theory of computable numbers is ill-defined.

I could be misinterpreting our notion of a "first-order theory of (some
subset of) the reals." It could be that when we (in this discussion, at
least) talk about the first-order theory of polynomially-approximable
numbers we mean the set of formulas which both:
1. Make use only of the + and * functions, and the < and = relations
2. Are true when interpreted in a model consisting only of numbers which
    can be approximated in polynomial time, regardless of whether the
    formula itself can be validated in polynomial time.

If this is what we mean, then it would be fair to say that when your
model is any superset of the algebraic numbers, the set of sentences
which are true in this model is exactly the same as the set of
sentences which is true for all the reals, and so Tarski's celebrated
decision procedure can always determine whether a sentence is true in
finite time. But I would argue that this is not what people usually
mean when they talk about "constructive" or "computable" theories,
largely because there isn't much to discuss: if your chosen
"computable" subset of the reals includes the algebraic numbers, then
the theory is complete and decidable, end of story. It is far more
common to focus on the case where the predicates (equality and the
inequalities) are also computable. But once you do this, as I mentioned
in an earlier post, you lose the axiom that "a <= b or b <= a for all
a,b" and in so doing weaken your theory from the standard, classical
theory of the reals to a Bishop-style theory in which Tarski's decision
procedure doesn't hold.

Regards,
Anthony