wtf wrote: ↑Tue Mar 19, 2024 5:00 am
Surely even formalists -- I thought I knew what formalism was but you are using it in a way that confuses me. Surely even a formalist would agree that there is a distinction between a decimal string matching that regex, and a real number.
The true nature of a number is unknown. We only know its various representations, i.e. its Platonic shadows.
I think that the various ontologies of mathematics, i.e. Platonism, structuralism, logicism, constructivism, and formalism are all simultaneously true. The relevant ontology depends on the context. Formalism is at its most relevant when denying the search for "meaning", i.e. impurity, and when rejecting arguments that are based on arguing such inexistent meaning. There is no meaning. Therefore, every argument that tries to argue "meaning", is wrong.
wtf wrote: ↑Tue Mar 19, 2024 5:00 am
After all, does our formalist friend recognize pi as
4(1 - 1/3 + 1/5 - 1/7 + 1/9 - ...), the famous
Leibniz series?
Pi is indeed very well represented as a constructivist program, i.e. an algorithm, which can again be represented as a string. In fact, all numbers are algorithms. A number, as represented by its program, is simply another Platonic shadow of the same unknown thing.
wtf wrote: ↑Tue Mar 19, 2024 5:00 am
It seems to me that the best you could do would be to define the number pi as the equivalence class of all the string expressions that can be proven equal to that number under whatever axiom system you're in, say ZFC.
Yes, every equivalence requires a proof. There are infinitely many programs representing the same number. A program is also a string expression. Proving that two programs represent the same number, implicitly requires proving that these two programs both terminate or not. Therefore, Turing's halting problem prevents the existence of a general program that can determine if any two arbitrary number programs represent the same number. Therefore, this equivalence class cannot be constructed.
wtf wrote: ↑Tue Mar 19, 2024 5:00 am
Even so, every time someone proves a new equality, they're finding another "pointer" to the number that they didn't know about before. You have to add it to your equivalence class. Meaning that it really WAS in that equivalence class BEFORE you discovered it.
Yes, agreed, but this set cannot be defined, because its membership function requires solving Turing's halting problem.
wtf wrote: ↑Tue Mar 19, 2024 5:00 am
Conclusion: Even a formalist, in the end, has to admit that either there's something "out there" being pointed to, like the number represented by pi, or else their definition of the number pi is historically contingent, because they can never know ALL of the expressions that will someday be discovered to evaluate to pi.
Yes, agreed, but formalism is not a rejection of Platonism. Formalism is the rejection of attributing meaning to purely Platonic abstractions. Realism works as well as anti-realism in mathematics. Realism is useful but not necessary.
wtf wrote: ↑Tue Mar 19, 2024 5:00 am
Did this make sense? It's a little abstract but it makes perfect sense to me. Let me know if it's not clear. I'm just trying to understand how you're using the word formalism. I can't imagine defining pi as the expression 3.14159... You'd be privileging one representation over another.
And how do you even know what the digits are? You need to be given an algorithm that computes them. And the algorithm exists independently of your knowing about it. So even formalists must believe in SOMETHING. You can't be a formalist in a vat.
Formalism points out that realism is not necessary. Formalism is an antidote to the bad practice of insisting on impurity, i.e. "meaning". The idea that Platonic abstractions truly exist in their own universe, is not a problem at all, as long as we understand that these abstract objects are essentially meaningless.