From Harvey Friedman's [manuscript][1] on "Order Invariant Relations and Incompleteness": > DEFINITION 4.4. A $\Pi_1^0$ sentence is a sentence asserting that some given Turing machine never halts at the empty input tape. A $\Pi_2^0$ sentence is a sentence asserting that some given Turing machine halts at every input tape. Let mathematical existence mean no more than consistency of an otherwise arbitrary definition. Let physical existence be based on observations and experience. (Remember those arguments evoking the number of atoms in the universe?) Let philosophical existence mean that you either explicitly define what you mean by that word (like Quine did in [*On What There Is*][2]) or alternatively that you use your implicit ontological commitments (like Descartes did in [*ego cogito, ergo sum*][3]). A Turing machine seem to have some form of potential physical existence, but an oracle for $\Pi_1^0$ or $\Pi_2^0$ sentences should not claim any form of physical existence. *Or do I miss something here?* 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). This theorem doesn't seem equivalent to a $\Pi_1^0$ sentence. *Is it equivalent to a $\Pi_2^0$ sentence?* The two *questions* above feel reasonably precise and answerable to me. Below comes a more controversial question, which is my real motivation for asking this question here. Max Tegmark uses Turing machines to define existence in the old (2007) paper [The Mathematical Universe][4]. His approach seems to cover issues not addressed in the definitions above (which are based on [a question and its answers][5] about the logical implications from the existence of Turing machines, and on a [comment by H. Dieter Zeh][6] on Max Tegmark's proposal). At the same time it feels unpolished and slightly naive. (He only considers computations that terminate, but wants to substitute identity for equivalence to get rid of potentially undecidable equivalence classes.) But the idea to use Turing machines to define which infinite structures actually exists seems to better capture our intuitions why things like the natural numbers should exist, then the normal way to use Turing machines as a starting point to postulate the existence of halting oracles, and then trying to transfinitely postulate more powerful oracles into existence. *Have Max Tegmark's ideas been worked out in a less naive way in the meantime (or maybe even a long time ago), maybe even by Max Tegmark himself in follow up publications?* [1]: https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/ [2]: https://tu-dresden.de/die_tu_dresden/fakultaeten/philosophische_fakultaet/iph/thph/braeuer/lehre/metameta/Quine%20-%20On%20What%20There%20Is.pdf [3]: http://philosophy.stackexchange.com/questions/14101/are-there-any-other-things-like-cogito-ergo-sum-that-we-can-be-certain-of/14461#14461 [4]: http://arxiv.org/abs/0704.0646 [5]: http://philosophy.stackexchange.com/questions/14529/which-ontological-commitments-are-embedded-in-a-straightforward-turing-machine-m [6]: http://www.rzuser.uni-heidelberg.de/~as3/multiversemania.pdf