Which ontological commitments are embedded in a straightforward Turing machine model?

Question

Let's assume that in response to a question or problem, a certain type of idealized finite Turing machine can be presented as an answer as if it would really (=physically) exist. Is the corresponding ontological commitment from this assumption strong enough to prove certain (foundational) first order theories like Robinson arithmetic, WKL₀, Peano arithmetic or ZFC consistent? Is it at least strong enough to prove the completeness of first order predicate logic in a reasonable sense?

The type of idealized finite Turing machine I have in mind here is one with an infinite tape, empty except for a finite number of cells (the initial state of the tape), a finite number of internal states and a finite deterministic transition table. The machine can runs as long as is required to halt, or run forever if the HALT instruction is never encountered. This machine is idealized, because it can potentially run forever, and because the initial state and the transition table are allowed to contain an arbitrary finite (potentially unimaginable huge) amount of information.

I wonder especially whether the assumption of the existence of such idealized Turing machines is stronger than the mere assumption of the existence of the potential infinite corresponding to the initial state of the tape. By stronger, I mean that more statements about first order predicate logic can be proved based on this assumption.

Answer 1

My instincts here are pulling me towards the route of

Turing Machines -> Church Turing Thesis -> Curry-Howard Correspondance -> Proof Theory

The problem with this intuition is that in all of your suggested mathematical theories, we are already taking as background assumptions the full resources of first order classical predicate logic. The Proof theoretic resources following from Curry-Howard usually give us axiom schemes that we ought to already accept in that setting!

What might be interesting though would be the effect of slightly more powerful machines corresponding to subtheories of Second or Higher Order logic. At a glance, it looks like there has been some fun stuff following from developments of Girard's System F calculus - here's a paper by Philip Wadler that discusses the idea that there is a representation in second order lambda calculus of a large class of arithmetical functions, regardless of the addition of explicitly arithmetical axioms.

Answer 2

The assumption is strictly stronger than Robinson arithmetic. It allows us to assume that Π⁰₁ sentences from the arithmetic hierarchy have a "privileged ontological status". Because of the way I formulated the question, Π⁰₂ (unintentionally) fails to achieve a similar status. I conclude this because of Harvey Friedman's manuscript on "Order Invariant Relations and Incompleteness":

DEFINITION 4.4. A Π⁰₁ sentence is a sentence asserting that some given Turing machine never halts at the empty input tape. A Π⁰₂ sentence is a sentence asserting that some given Turing machine halts at every input tape.

Added 16. April 2016: It turns out that the "privileged ontological status" of Π⁰₁ sentences (or rather the absence of this status for Π⁰₂ sentences) is more than just an arbitrary unintentional artifact of formulation details. A Turing machine has a finite number of internal states, and an infinite tape, but it is unable to decide whether an infinite input is really infinite, or whether it would turn out to be finite after all, if it only continued reading it long enough. Here is another explanation:

I was recently surprised to find out that one can consistently accept the existence of Turing machines, and reject the existence of Turing machines with access to an oracle for deciding the halting problem problem of a Turing machine. This is because the oracle can lie (but one cannot prove that it lies) and claim that a non-halting computation would actually halt, and then taking forever while answering with an infinite number, when asked for a bound on the number of steps. (I realized this after writing a technical justification for the excuse: Then I might justify my doubts about Π⁰₂ sentences by explaining that I'm unsure about how to separate finite inputs from infinite inputs, and hence am unsure whether quantification over the inputs is well defined. That excuse itself arose from a conversation with another Thomas.)

---

If one is willing to grant the existence of a succession of increasingly more powerful oracle Turing machines, then one seems to be able to get ontological commitments "arbitrary close to the Church-Kleene ordinal", as explained here:

To answer your question, I claim that statements about Turing machines with halting oracles have definite truth values, just as “clearly” as statements about ordinary TMs do. The argument is simply this: you agree that any given Turing machine, on any given input, either halts or doesn’t halt? Well then, every call to a halting oracle has a definite right answer. Therefore, the operation of a TM with a halting oracle is mathematically well-defined at every point in time. Therefore, by the same intuition you used for ordinary TMs, you should conclude that the oracle TM either halts or doesn’t halt, and that there’s a definite fact of the matter about which it does.

Continuing recursively in this way gets you to definite truth-values for all Π⁰_k sentences, for any value of k—and actually further, to Π⁰_α sentences, where α is any computably-definable ordinal. But it doesn’t get you beyond that: it stops at the supremum of the computable ordinals, which is called the Church-Kleene ordinal. Beyond that lies the enchanted realm of the Axiom of Choice and the Continuum Hypothesis, for which I don’t think one has to admit the existence of any well-defined truth value (though neither is one prohibited from doing so).

Edit: On closer reading, this is actually a misinterpretation from my side. We don't get the well-order of those ordinals (we have to somehow know that they are well-ordered), we just get that Π⁰_α sentences have definite truth values (for the mentioned ordinals α).

---

These two answers are not necessarily in the direction that I initially intended this question, but they seem to describe the ontological commitments that people in practice derive based on assumptions related to the existence of (powerful oracle) Turing machines. This answer is quite unpolished, but who cares anyway? Later...

Answer 3

It is fairly straight-forward to construct a Turing machine from a given finite start space and a given Turing machine that, in a finite number of states and finite amount of time (which is constant) produces a given start state and then runs the given Turing machine on the input.

That is to say, it reduces to standard computation.