The question whether some postulated structure (like ZFC) has mathematical existence is equivalent to a $\Pi_1^0$ sentence. The link between consistency and existence is provided by the model existence theorem of first order logic (i.e. the completeness theorem). ... No, the model existence theorem is not equivalent to a $\Pi_2^0$ sentence! OK, but what is the connection between the model existence theorem and (oracle) Turing machines?
A $\Pi_k^0$-TM is a normal Turing machine if $k=0$, and a Turing machine with access to an oracle for deciding $\Pi_k^0$ sentences otherwise. Let TT be a given first order theory whose axioms are enumerable by a $\Pi_k^0$-TM. The question whether TT is consistent is equivalent to a $\Pi_{k+1}^0$ sentence. The question whether TT is negation complete is equivalent to a $\Pi_{k+2}^0$ sentence. In the first case the $\Pi_k^0$-TM enumerates all valid proofs, and stops if it finds a proof of a contradiction. In the second case, the input is a formula $\varphi$, the $\Pi_k^0$-TM enumerates all valid proofs, and stops if it finds a proof of $\varphi$ or a proof of $\lnot\varphi$.
A theory contains examples, if for every formula of the form $\exists x\varphi$, there exists a term $t$ such that $(\exists x\varphi\to\varphi\frac{t}{x})$ is provable. Let TT' be a first order theory whose axioms are enumerable by a $\Pi_{k'}^0$-TM. If TT' is consistent, negation complete and contains examples, then it has a canonical model based on the term algebra under an equivalence relation decidable by a $\Pi_{k'}^0$-TM, which also decides the atomic relations evaluated on terms. (The $\Pi_{k'}^0$-TM decides any formula $\varphi$ by simultaneously searching for a proof of $\varphi$ and a proof of $\lnot\varphi$.)
How does the model existence theorem fits in? The (ontologically) critical part of the model existence theorem asserts the existence of a specific first order theory TT', whose axioms are enumerable by a $\Pi_{k+1}^0$-TM and include the axioms of TT. It is asserted that TT' is consistent iff TT is consistent, and that TT' is negation complete and contains examples. The (mathematical) existence of $\Pi_{k+1}^0$-TMs is just assumed without proof. I wonder whether this assumed (mathematical or philosophical) existence could be justified based on the ontological commitments implied by the existence of $\Pi_k^0$-TMs and by talking about consistency (i.e. $\Pi_{k+1}^0$ sentences) and negation completeness (i.e. $\Pi_{k+2}^0$ sentences).
Edit I recently learned that the above proof of the model existence theorem is a "de re" proof, at least with respect to the part "The (mathematical) existence of $\Pi_{k+1}^0$-TMs is just assumed without proof." There is a weaker "de dicto" proof which only needs the weak König's lemma instead, and just proves existence without constructing any specific model. I also learned that the above "de re" proof basically needs ACA0, or rather that $\Sigma_1^0$ comprehension is already equivalent to ACA0 over RCA0 (see Lemma I.4). So there is a connection to the reverse mathematics perspective, even so the ontological perspective gives slightly different answers.
A Turing machine seems to have some form of potential physical existence, but an oracle for deciding $\Pi_1^0$ or $\Pi_2^0$ sentences should not claim any form of physical existence. Or do I miss something here? ... Yes, I'm missing something! OK, but where else can one draw the line between physical and mathematical (or philosophical) existence?
Here is an incomplete list of some things which I'm missing here:
- Because potential physical existence is some form of philosophical existence different from physical existence, I would either have to explicitly define what I mean by it, or alternatively use my implicit ontological commitments.
- That I can't decide arbitrary $\Pi_1^0$ sentences doesn't necessarily mean that my all powerful opponent cannot do it either. Maybe he just guesses the answer (if his enormous computational powers should fail to provide him a certain answer), and is so extremely lucky that he guesses right each time (when he plays against an inferior being like me). N J Wildberger's new logical principle: "Don’t pretend that you can do something that you can’t." misses the same point. So physical existence can involve randomness and multiple interacting parties, and having probability zero is different from being impossible, because there might be infinitely many similar events also having probability zero. But N J Wildberger would probably happily bite the bullet, and answer his opponent who claims that a given (undecidable) TM will never halt that it will halt in less than $c=10^{10^{10^{10^{10}}}}$ steps, knowing that his opponent will be unable to refute that statement.
- I want to assume the existence of Turing machines, not because I really believe in their physical existence, but because I believe that they will provide a useful and wide ranging abstraction. I want to assume that a $\Pi_1^0$ sentence is either true or false, because I want falsifiable statements like statements about consistency to be either true or false. I don't really know what I want for $\Pi_2^0$ sentences. Many statements of practical interest are $\Pi_2^0$ sentences, so I might be willing to bite the bullet and admit that even some unpractical $\Pi_2^0$ sentences like Goodstein's theorem are true, and that if fact every $\Pi_2^0$ sentence is either true or false. But if this would mean that I also have to admit that every $\Pi_3^0$ sentence is either true or false, than I may prefer to already deny this for $\Pi_2^0$ sentences. But all those reason are very subjective, so they don't even constitute objective ontological commitments.
Can one draw a line between different forms of existence somewhere? Maybe, but this question and answer revolve around Turing machines, $\Pi_1^0$, $\Pi_2^0$ sentences, and $\Pi_1^0$-TM, so let's try to stay in that context. It seems out of context to wonder whether models of Peano arithmetic constructed by the model existence theorem are $\omega$-inconsistent. But it should be ok to look at Quine's criteria for philosophical existence, namely to ask myself whether I'm willing to quantify over the objects claimed to exist. Then I might justify my doubts about $\Pi_2^0$ 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. What happens if we modify the definitions of $\Pi_1^0$ and $\Pi_2^0$ sentences such that $\Pi_1^0$ quantifies over the input and $\Pi_2^0$ does not?
A $\Pi_1^0$ sentence is a sentence asserting that some given Turing machine never halts at every input tape. A $\Pi_2^0$ sentence is a sentence asserting that some given $\Pi_1^0$-TM never halts at the empty input tape.
If the TM halts for a given input, then it has only read a finite part of the input, so it doesn't matter that also infinite inputs might be present. Let's assume that it is obvious that the two definitions of $\Pi_1^0$ sentences are equivalent, and only verify the equivalence for the two definitons of $\Pi_2^0$ sentences. If a $\Pi_2^0$ sentence is given by a Turing machine, then the $\Pi_1^0$-TM asks the $\Pi_1^0$ oracle for each possible input whether the corrsponding Turing machine will not stop, and halts if the oracle confirms this. So the $\Pi_1^0$-TM will not halt exactly if the $\Pi_2^0$ sentence is true. QED. If a $\Pi_2^0$ sentence is given by a $\Pi_1^0$-TM, let the input describe the hypothetical answers of an $\Pi_1^0$ oracle for the first $n$-queries, where the oracle also gives a bound on the number of steps if Turing machine (of the query) is supposed to halt. The Turing machine then first checks whether the $\Pi_1^0$-TM halts in $n$-steps for those answers of the oracle, and then checks whether the halting predictions were correct. After that, it starts to verify the non-halting predictions, which will take forever exactly if it cannot refute them. So there will be an input for which the Turing machine does not halt, exaclty if the $\Pi_1^0$-TM halts in a finite number or steps. QED. So if the oracle lies and claims that a Turing machine halts even so it does not, this lie will translate into the bound on the number of steps being a never ending input sequence (if unary or binary notation is used). The Turing machine cannot know this, so it continues to read that infinite bound for ever (and never halts), without verifying that the $\Pi_1^0$-TM did halt in a finite number of steps. This indicates that I might indeed be able to accept that all $\Pi_1^0$ sentences are either true or false without necessarily accepting the same for $\Pi_2^0$ sentences.
Can Turing machines clarify mathematical, philosophical, and physical existence?
Thomas Benjamin's reference to the Church-Turing thesis is relevant here, because Gödel indeed confirmed that Turing machines clarified things for him, while he was not yet convinced by Church's earlier work. However, physical existence is not clarified by this, and it isn't clarified by the above answer either. The removed reference to Max Tegmark's work at least tried to seriously consider physical existence. Maybe Andrej Bauer's about mutually inconsistent entities and my reply that physical and mathematical existence takes place in different universes are related to expectations about physical existence.
This answer is quite long, and mostly just tried to translate some known facts about mathematical and philosophical existence into the language of (oracle) Turing machines and see what they mean in that context. Translating the statements about (oracle) Turing machines back into the original language would probably only yield weaker statements than the original theorems. Is there anything which was really clarified by this translation? Yes, the fact that the $\Pi_{k'}^0$-TM, which decides the equivalence relation and the atomic relations, must also exist in addition to the set/collection on which we form the equivalence classes for building the model was illuminating for me. A similar observation that it is easy to underestimate the importance of equivalence relations or partitions for questions about existence was also made by David Ellerman. Also helpful for me was to realize that Quine's principle allows to deny existence of objects which aren't defined sufficiently unambiguous, even if we grant the existence of some explicit examples of such objects. The indices $k'$, $k+1$, and $k+2$ in the translation of the model existence theorem also seem helpful to me.
