5 ms·

From the point of view of proof-theory, you can show that PA (arithmetic) is equivalent to the consistency of the omega cardinal (the countable infinite). Basic

From the point of view of proof-theory, you can show that PA (arithmetic) is equivalent to the consistency of the omega cardinal (the countable infinite). Basically, everything line up quite well between things you want to be true and things that are true in that system. This equivalence breaks down with higher-order system such as System F, but it gives a system that may feel more natural, especially to programmers. The problem that explains the endurance of "formalism" is that there are so many things that you "want to be true" that can't be shown to be true in intuitionistic systems is a real issue. For instance, simply proving that a fast-growing function is total. You are fine with recurrence, but not if the function grows too fast? This sounds really stupid. But I don't think many people care that much, they'll just use whatever give them results.

btilly 1y ago
It is certainly easier to prove interesting theorems with formalism. You don't get caught up with such basic things like whether or not it is always possible to tell that one real number is bigger than another. But formalism leads to having to accept conclusions that some of us don't like. I already referred to the existence of uncountably many things that cannot in any useful way ever be specified. If you include the axiom of choice, you get the Banach-Tarski paradox. Mathematicians debated that one for a while, but now generally accept it. My favorite example of a weird conclusion comes from https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theo.... We can non-constructively prove the following facts. Any class of graphs that is closed under the graph minor operation (for example planar graphs), has a finite set of forbidden graph minors that completely characterize the graph (in the case of planar graphs, K5 and K3,3). In general, there is no way to find those forbidden graph minors. Even if you were given the complete list, you couldn't necessarily verify that the list was correct. You cannot necessarily even find an upper bound on how big this set is. By "cannot necessarily" I mean, "it is sometimes unprovable". In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size? To make this concrete, there are 17,523 known forbidden minors for the toroidal graphs. We don't know how to find more. We don't know if we have the full list. And we don't have an upper bound on how many more of them there are to be found. You're free to accept this ephemeral claim to existence as actual existence. But this existence isn't very useful for us.
- woolion 1y ago
  I'm fine with that. I don't think it's much worse than the quirks of what you call non-formalists systems. In your original comment, you mention: All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth. If you wanted to formalize something like that, you'd need the consistency of an absurdly large cardinal. I think it is an interesting type of question to explore, so it's fine to have these large cardinals.
  - btilly 1y ago
    I believe that you're fine with it, simply because that is what you're familiar with. And if you'd grown up with a different way of thinking about these problems, then you wouldn't be fine with it. Personally, I can work with either system. But, to me, formalism really does feel like a game. And the more that I have thought about the foundations of math, the more dissatisfied I have become with this game. And now I find myself frustrated when people assert the conclusions of the game as truth, instead of as merely being formal statements within a game that mathematicians are choosing to play. Here is something that I believe. We owe our current understanding of uncountability to Cantor's metaphor, about figuring out which group of sheep is larger by pairing them off. We would today have a very different kind of mathematics if Cantor had instead made a more careful analogy to the problem of trying to count all of the sheep that have ever existed. Even if you had perfect information about the past, you're doomed to fail because you can't figure out where to draw the line between ancestral sheep, and sheep-like ancestors. This second metaphor is exactly parallel to uncountability within the computable universe. For example we can implement reals as some kind of Cauchy sequences. For example as programs for functions f, where f(n) is a rational, and |f(n) - f(m)| <= 1/n + 1/m. This works perfectly well. But now Cantor's diagonalization argument clearly does not demonstrate that there are more reals. Instead it demonstrates the limits of what computation can predict about the behavior of other computations. In other words, I just described a system operating on a notion of truth that is directly tied to the reasoning required to establish that truth. And in that system, uncountable is tied to self-reference. And really doesn't mean more. I don't know how to really formalize this idea. But I'd be interested if anyone actually has done so.

btilly 1y ago

It is certainly easier to prove interesting theorems with formalism. You don't get caught up with such basic things like whether or not it is always possible to tell that one real number is bigger than another. But formalism leads to having to accept conclusions that some of us don't like. I already referred to the existence of uncountably many things that cannot in any useful way ever be specified. If you include the axiom of choice, you get the Banach-Tarski paradox. Mathematicians debated that one for a while, but now generally accept it. My favorite example of a weird conclusion comes from https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theo.... We can non-constructively prove the following facts. Any class of graphs that is closed under the graph minor operation (for example planar graphs), has a finite set of forbidden graph minors that completely characterize the graph (in the case of planar graphs, K5 and K3,3). In general, there is no way to find those forbidden graph minors. Even if you were given the complete list, you couldn't necessarily verify that the list was correct. You cannot necessarily even find an upper bound on how big this set is. By "cannot necessarily" I mean, "it is sometimes unprovable". In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size? To make this concrete, there are 17,523 known forbidden minors for the toroidal graphs. We don't know how to find more. We don't know if we have the full list. And we don't have an upper bound on how many more of them there are to be found. You're free to accept this ephemeral claim to existence as actual existence. But this existence isn't very useful for us.

woolion 1y ago
I'm fine with that. I don't think it's much worse than the quirks of what you call non-formalists systems. In your original comment, you mention: All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth. If you wanted to formalize something like that, you'd need the consistency of an absurdly large cardinal. I think it is an interesting type of question to explore, so it's fine to have these large cardinals.
- btilly 1y ago
  I believe that you're fine with it, simply because that is what you're familiar with. And if you'd grown up with a different way of thinking about these problems, then you wouldn't be fine with it. Personally, I can work with either system. But, to me, formalism really does feel like a game. And the more that I have thought about the foundations of math, the more dissatisfied I have become with this game. And now I find myself frustrated when people assert the conclusions of the game as truth, instead of as merely being formal statements within a game that mathematicians are choosing to play. Here is something that I believe. We owe our current understanding of uncountability to Cantor's metaphor, about figuring out which group of sheep is larger by pairing them off. We would today have a very different kind of mathematics if Cantor had instead made a more careful analogy to the problem of trying to count all of the sheep that have ever existed. Even if you had perfect information about the past, you're doomed to fail because you can't figure out where to draw the line between ancestral sheep, and sheep-like ancestors. This second metaphor is exactly parallel to uncountability within the computable universe. For example we can implement reals as some kind of Cauchy sequences. For example as programs for functions f, where f(n) is a rational, and |f(n) - f(m)| <= 1/n + 1/m. This works perfectly well. But now Cantor's diagonalization argument clearly does not demonstrate that there are more reals. Instead it demonstrates the limits of what computation can predict about the behavior of other computations. In other words, I just described a system operating on a notion of truth that is directly tied to the reasoning required to establish that truth. And in that system, uncountable is tied to self-reference. And really doesn't mean more. I don't know how to really formalize this idea. But I'd be interested if anyone actually has done so.