FOM: Small Turing Machines that transcend formal theories (response to Friedman)

[Joe Shipman]

Friedman:
>But what if we fix the presentation of Turing machines to be reasonably

>natural, in advance, and then change the theories?

>As a simplified example, suppose we are interested in the size of the
>smallest Turing machine TM which does not halt but cannot be proved to
not
>halt in PA or ZFC. How do these sizes compare?

It is easy to make a fairly small 1-tape 2-symbol Turing machine which
always halts when given an input tape consisting of a consecutive string
of n 1's beginning at and extending to the left of the initial cell,
such that this always-halting property is not provable in Primitive
Recursive Arithmetic.

This is because you can represent the polynomial a_n(x^n)+...+a_0 by the
string 111...(a_n+1 of these)..110111...(a_(n-1)+1 of these)....11011...
... 0111...(a_0+1 of these)...11 and play the game "considering the
polynomial as a base b representation of an integer, subtract 1 and then
increase b by 1, starting on input n with the polynomial x^n and base
2".  To prove this always halts requires transfinite induction up to
omega^omega.  The Turing machine would have only a few dozen quintuples.

To get a particular individual TM which does not halt but for which this
fact can't be proved in PRA seems quite a bit harder.  In general,
statements of the form

(1) "Machine M1 calculates a total function"

seem to be more tractable for proving transcendence over theories than
statements of the form

(2)"Machine M2 never halts".

Does anyone know of a general way for converting a statement of form
(1), unprovable in Theory T, into a statement of form (2) unprovable in
theory T, that is not as horrible as making an M2 that searches for
proofs in T that M1 calculates a total function?


To transcend PA rather than PRA, you can do something similar to the
above except you have to represent numbers by exponential polynomials
("pure base b" rather than base b -- for example, 397 in base 10 would
be represented in base 3 as 3^5+3^4+2*3^3+2*3^2+1 but in "pure base 3"
as 3^(3^1+2) + 3^(3^1+1) + 2*3^(3^1) + 2*3^2 +1).  The difficult part is
figuring out how to conveniently represent the tree-like structure on a
linear tape so that the operation of subtracting 1 can be done in a
"local" way.  There is probably an elegant solution to this but I don't
know it -- it's probably not too hard if you allow multi-tape machines.

I have no idea how you would transcend ZF with a small Turing machine;
maybe Harvey can formulate a finite form of one of his Boolean Relation
Theory independence results that is optimized for this.

-- Joe Shipman