How much platonism do I need to handle the halting property?

Question

I always considered myself as platonist (in contrast to formalist / finitist) but recently I realized (if this is actually true) that you need a bit of platonism to even make sense of questions like 'is ZFC consistent' or, given a specific code, 'will this program halt'. Because asking these questions presumes the existence of the inifinite set of derivations from ZFC or an infinite amount of computational ressources. As a formalist, I feel, I'm only allowed to ask questions like 'will we find a contradiction in ZFC' or 'will we ever build a machine which halts on this program'.

Is this interpretation of platonism actually true? If yes, what is the minimal amount of platonism needed to make sense of the questions stated above?

Answer 1

This is more a finitist vs non-finitist issue than it is about Platonism or formalism: Admitting that For no integer P(x) holds is sensible statement for a decidable property P is compatible with formalism, and indeed most approaches to mathematics.

But even the finitist is not very far removed from the others: As pointed out in the question, she cannot make sense of the statement above as written. However, she can still resort to I will never find an integer such that P(x). The platonist might think that the finitist is making a different statement - after all, if the shortest ZFC-derivation of 0=1 is longer than the number of particles in the universe, the platonist would deem ZFC to be inconsistent, whereas the finistist still sees ZFC as consistent. However, the finitist does not consider this a meaningful objection, anyway. In either case, neither the platonist nor the finitist has a way to prove such a statement anyway.

Answer 2

Any absolute statement about the future is subject to change. Will it snow where I am on February 19, 2020? That's impossible to say as of February 19, 2019. Will we find a contradiction in ZFC? Even if there is one, it's impossible to answer. Maybe all mathematicians are killed in the mindworm invasion of 2021, and nothing is ever derived again. Maybe nobody stumbles across it in the next few trillion years (after which we don't have working stars, and presumably no mathematicians).

It's possible to ask if something might happen. The world might continue as it is for another year. I'm very likely to live another year. I might live where I am currently, and February snowfall is reasonably common here. Therefore, it definitely might snow where I live in a year.

So, given a program, might we build a machine running that program that halts? If it halts, it halts in finite time, in a finite number of states, and therefore is of finite size. If that program can halt it's possible that we will build a machine that will halt on it, provided we have enough resources. If we disregard infinite-length mathematical derivations, and that's at least a reasonable stance, the same is true of finding a contradiction in ZFC if there is one.

Let's consider resources. The Universe is a big place, and as far as we know the last stars won't go out for a few trillion years. It's still finite, and it's possible to imagine something bigger than the observable Universe, or something that will take longer than a few trillion years. Can we be sure that the observable Universe is all that we will ever have access to? It's not that we have assurance that we know all the laws of natural and potentially supernatural physics, so it's conceivable that we can get more resources over the next billion years or so.

So, the answer to "will we..." is unknowable until something does or doesn't happen, and the answer to "Could we build a machine program X halts on" is the same as the answer to "Does X halt under some circumstances?"

Answer 3

There really are, to some degree 'levels of Platonism". "Will we ever find a machine that halts on this program" does not necessarily require infinite resources to answer either positively or negatively. And different 'levels' in the continuum between Ultra-Finitism and true Platonism will give different answers.

For many programs, you can answer the question positively by inspecting the program and constructing one that does. That does not require infinite resources. But it may require a level of resource consumption that is excessive and incomprehensible.

The Ultra-Finitist would put a definite limit on how fast your constructed machine would have to run in order to be considered 'real'.

A mere Finitist would find it sufficient that you can put a boundary, any boundary on how long the machine could run.

A Constructivist would find it sufficient to prove that if the machine did not halt, then some other problem of know difficulty could be solved faster than we know it can.

An Intuitionist would find it sufficient even if the machine could not be directly produced, but if it were the limit point of some progression of more and more complex machines that halt on related problems of increasing complexity, as long as the complexity of the problem increases faster than the complexity of the machine and eventually overtakes it.

A Classical Formalist would find it sufficient if there is a contradiction between the halting not happening and some other definable infinite structure not being complete. For instance a diagonal argument such as the one that proves the reals are not countable. So there would not be a construction, or a general rule for construction, but an infinite list of things that can be defined, and that would not exist were there no such machine.

A Platonist would not even require the infinite structure to be definable in the strict sense, only that its existence should be consistent with logic.

The range of allowed negative answers is similar. A contradiction is a constructed object that contradicts the existence of another constructed object.

Each step on this ladder believes in contradictions that are as materially constructed as they allow their real objects to be. Contradictions that are less clear rule out proving the result, but they do not prove it false. They leave successively smaller gaps of the irrelevant or unknowable between the true and the false. Nowadays, since we have thought up things like Russel's set and the Barry's number, even a sane Platonist must allow for this gap, since clear language still contains paradoxes.

There are rungs between and beside these points as well, but it is harder to nail down precisely what those mean. In particular, modern Set Theory like the theories of Large Cardinals, dwell in the middle ground between Classical Formalism and Platonism, allowing infinite constructions via transfinite induction across all ordinals, but not arbitrary combinations of other ungrounded collections.