User:Yto

Hi, i've been an apeirologist for approximately 4 years. I thought about writing articles on this wiki, but realized that i'm bad at finding sources, so i'll just use this page for unsourced explanations and philosophy related to apeirology. Hopefully that's ok.

Platonism

1. Introduction

Platonism is the philosophy of Plato. It asserts that abstract objects such as beauty and injustice exist. In the context of mathematics (mainly set theory), i think "platonism" commonly refers to a view asserting that something has a value independent of our thoughts. For example, a platonist may believe in an independent universe of sets, or only in an independent set of natural numbers. Due to this variety, platonism is not a single belief, but a way to compare beliefs - one belief is "more platonic" than another if it asserts that more things are independent of thoughts. A view with absolutely no platonism is pointless, because that would mean nothing can be certain, not even statements such as 1+1=2, or the existence of anything at all.

For example, if we abandon the idea that there is no integer between 0 and 1, despite this being true in our physical world, there are suddenly many things we cannot be certain about. What if 7 is the largest prime number, and all the larger numbers that we call "primes" are actually divisible by this hidden integer n? How would a function with n inputs work? Is 2+2 still 4, or could it now be 3? Maybe 2+2 is an integer between 3 and 4. Being too unplatonic leads to confusing (but entertaining) questions like this, and if we want to get any advanced results, it's more useful to simply assume that some things are the way we expect them to be.

2. Social and formal proofs

There are two kinds of proofs in math. Formal proofs start with specified axioms and use well-defined rules to make inferences. Meanwhile, social proofs don't necessarily start with any axioms, and inferences can be made intuitively. The goal of a social proof is to convince the reader that something is true, while the goal of a formal proof is to show that if the axioms are true, then the theorems are also true, therefore a social proof of the axioms would lead to a social proof of the theorems. A perfect example of social proofs are visual proofs.

This is closely related to platonism. A more platonic view allows more social proofs. For example, the belief that the axioms of Peano arithmetic are true independently of our thoughts basically directly assigns social proofs to all formal proofs in Peano arithmetic. However, a belief in an independent set of natural numbers can lead to social proofs of much more, probably including things like the consistency of Peano arithmetic. It also implies that there are independent truth values of the twin prime conjecture and the goldbach conjecture, but we don't have any social proofs of those truth values yet, and i don't know whether it's possible that social proofs of these would require a more platonic view, or even not exist at all.

Of course, as i mentioned in the introduction, there are views so unplatonic that they allow the existence of integers between our usual integers, or perhaps even the non-existence of our usual integers. With these views, even formal proofs are in danger, as for example certain things that look like formal proofs to us may actually just not exist at all, or may contain inferences that look like they're allowed but aren't. This makes formal proofs also a little social, so the main distinction between social and formal proofs is that formal proofs can be verified by a computer. But again, while it can be entertaining to think this way, it's unlikely to be productive.

3. Different kinds of well-definedness

For apeirology, platonism is relevant because the well-definedness of certain things may depend on what kinds of proofs are allowed, and this depends on the view. A view that isn't platonic enough can put an upper bound on the size of well-defined ordinals, or on the growth rate of well-defined functions for finite numbers. Weirdly enough, it also depends on what kind of well-definedness we're interested in.

Well-definedness seems like a straightforward idea - something is well-defined if it has a unique value. We can, for example, easily prove the well-definedness of the busy beaver function - it's clear that for every n, there are finitely many halting n-state turing machines, so there's a finite set of numbers of ones left after halting, and we can take the maximum of that set. This can be proven formally. However, no matter what consistent recursive theory you work in, you can't prove each value of the busy beaver function constructively. Assuming ZFC is consistent, even if you knew the specific value of BB(800), you can't prove in ZFC that BB(800) is equal to that value, because there's a turing machine with 748 states that halts iff ZFC is inconsistent, and ZFC can't disprove that. Even if ZFC could prove that the machine can't halt with more than the claimed value of BB(800) ones on the tape, there probably is a simple way to prevent that with the 52 extra states. For stronger theories, we can just increase the input and the same thing will apply. So is the busy beaver function really well-defined?

This is where the different kinds of well-definedness come in. There are at least 4 important ones when it comes to functions (i haven't yet thought about this for anything else, sorry), which may have actual names already, but i would have to look for sources so i just gave them some placeholder names for now: Nonconstructive individual (NI) well-definedness, Nonconstructive global (NG) well-definedness, Constructive individual (CI) well-definedness, and Constructive global (CG) well-definedness.

A function f is NI well-defined in T iff for every x in f's domain, T can prove there's a unique y such that f(x)=y.

A function f is NG well-defined in T iff T can prove that for every x in f's domain, there's a unique y such that f(x)=y.

A function f is CI well-defined in T iff for every x in f's domain, there's a unique y such that T can prove f(x)=y.

The only difference between these three is the position of "T can prove" in the definition, and it's an important difference. Anyway, onto the fourth kind of well-definedness: A function f is CG well-defined in T iff it's both NG and CI well-defined in T. It's worth noting that when T is a relatively nice theory, NG well-definedness in T implies NI well-definedness in T, and so does CI well-definedness in T, so these 4 kinds of well-definedness form a sort of square of implications.

So if we allow only formal proofs, then all CI well-defined functions are computable. That excludes BB, which i've shown above, but also Rayo's function and every Kleene's O. There are even problems with NG well-definedness of Rayo's function, although those can be fixed by using a second-order theory (which still doesn't fix CI well-definedness). Now, this is just my opinion, but i think CG well-definedness is the main kind of well-definedness we should be interested in, and that is one of the biggest reasons why my view is very platonic - allowing social proofs makes many NG well-defined things also CG well-defined.

I'll try to add more to this eventually.