Comment by woolion

Comment by woolion 5 days ago

24 replies

View on Hacker News

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 5 days 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_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.

Reply View 23 replies
  • pron 5 days ago

    > In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size?

    In the same sense that we could say that every computer program must either eventually terminate or never terminate without most people thinking there's a major philosophical problem here.

    And by the way, the very same question can be (and has been) levelled at constructivism: in what sense does a result that would take longer than the lifetime of the universe to compute exist, as it is unfindable and unverifiable?

    Look, I think that it is interesting to work with constructive axioms, but I don't think that humans philosophically reject non-constructive results. It's one thing to say that we can learn interesting things in constructive mathematics and another to say there's a fundamental problem with non-constructive mathematics.

    > But formalism leads to having to accept conclusions that some of us don't like.

    At least in Hilbert's sense, I don't think formalism says quite what you claim it says. He says that some mathematical statements or results apply to things we can see in the world and could be assigned meaning through, say, correspondence to physics. But other mathematical statements don't say anything about the physical world, and therefore the question of their "actual meaning" is not reason to reject them as long as they don't lead to "real" results (in the first class of statements) that contradict physical reality.

    Formalism, therefore, doesn't require you to accept or reject any particular meaning that the second class of statements may or may not have. If a statement in the second class says that some set exists, you don't have to assign that "existence" any meaning beyond the formula itself.

    Reply View 16 replies
    • zozbot234 5 days ago

      > Look, I think that it is interesting to work with constructive axioms, but I don't think that humans philosophically reject non-constructive results.

      I don't think the point of constructivism is to "philosophically reject non-constructive results". You can accept non-constructive results just fine as a constructivist, so long as they're consistently rephrased as negative statements, i.e. logical statements starting with "NOT ...". This is handy in some ways (you now know instantly what statements correspond to "direct" proofs that can be given a computational semantics and even be reused for all sorts of computer sciencey stuff) and not so handy in others (to some extent, it comes with a kind of denial about the inherently "dual" nature of the fragment of your constructive logic that contains all that negatively-phrased stuff). But these are matters of aesthetics and perceived elegance, more than philosophy.

      The duality concern is one that some will want to address by moving even further to linear logics (since these are "dual" like classical logic but also allow for constructive statements) but of course that's yet another can of worms in its own right.

      Reply View 2 replies
      • btilly 5 days ago

        When you talk about the point of constructivism, do you mean currently, or historically?

        For me, personally, the point of constructivism is to wind up talking about mathematics in a language that corresponds with what I want words to mean. I personally want mathematical existence to mean something that could be represented in an ideal computer. And existence in classical mathematics means something very different than that.

        But historically, the point of constructivism was to try to avoid paradoxes through careful reasoning. At least that is my understanding. You're welcome to read http://thatmarcusfamily.org/philosophy/Course_Websites/Readi... and decide if that is what Brouwer meant.

        Unfortunately for this historical motivation, Gödel proved that every classical mathematical proof can be mechanically transformed into a purely constructive proof, possibly of a much more carefully worded statement. With the result that if there is a contradiction within classical mathematics, there is also a contradiction within constructivism.

        Luckily it has been so long since our foundations of mathematics fell apart because of someone finding a contradiction, that we no longer worry about it. (Was the set of all sets that do not contain themselves the last such contradiction? I think it might have been.)

        Reply View 1 reply
        • zozbot234 4 days ago

          You could argue that the early constructivists' notions of "paradoxes" included things such as "statements about the existence of things that we don't know how to explicitly construct, and that may be even impossible to explicitly construct in the general case". Under Gödel's argument, these statements (like other classical statements) become mere negative statements asserting the non-existence of anything that might contradict the aforementioned non-constructive objects. So, they're no longer "paradoxical" in that sense. Stated another way, decidability/computability (perhaps relative to some appropriate oracle, to fully account for the surprising strength of some loosely-"constructive" principles) is not quite the same concern as consistency. Of course, this was all stated in very fuzzy and imprecise terms to begin with (no real notion back then of what "decidable" and "computable" might mean), so there's that.

          Reply View 0 replies
    • btilly 5 days ago

      My understanding of how Hilbert meant it is summed up in this quote from him: "Mathematics is a game played according to certain simple rules with meaningless marks on paper." I think that in part because I read Constance Reid's excellent biography Hilbert! It traces in some detail his thinking over his life, and how he came to formalism. His thinking about the nature of existence was particularly interesting.

      If you think that he meant something else, please find somewhere where he said something that didn't boil down to that.

      As for what most people think about the philosophical implications, nobody should be expected to have any meaningful philosophical opinions about topics that they have not yet tried to think about. I know that I didn't.

      After you've thought about it, you may well have a dramatically different opinion than I do. For example Gödel thought that mathematical existence was real, since mathematics exists in God's mind. This idea made it important to him to decide which set of axioms was right, where right means, "These are the axioms that God must have settled on, and that therefore exist in His mind." This lead to such ironies as the fact that after proving that the consistency of ZF implies the consistency of ZFC, he then concluded that that the construction was so unnatural that Choice couldn't be one of God's axioms!

      I don't agree with Gödel. For a start, I don't believe that God exists. And after I thought about it more, I realized that what I want existence to mean, isn't what mathematicians mean when they say "exists". I'm willing to use language in their way when I'm talking to them. But I'm always aware that it doesn't mean what I want it to mean.

      Reply View 12 replies
      • ConspiracyFact a day ago

        I thought it was generally understood that Hilbert didn’t literally believe that. Do you seriously believe that he believed it?

        Reply View 1 reply
        • btilly a day ago

          What I said about Hilbert's belief was a quote by him. So of course I believe it.

          His full views were more complicated, and are already discussed elsewhere in this discussion.

          My statement about Gödel is not an exact quote, but fits what I've heard from every source on the topic. He was a very deeply religious genius.

          Reply View 0 replies
      • pron 5 days ago

        I can't locate my Heijenoort right now, but here's a description from the Stanford Encyclopedia of Philosophy [1] (which points to Heijenoort):

        The analogy with physics is striking... In the second half of the 1920s, Hilbert replaced the consistency program with a conservativity program: Formalized mathematics was to be considered by analogy with theoretical physics. The ultimate justification for the theoretical part lies in its conservativity over “real” mathematics: whenever theoretical, “ideal” mathematics proves a “real” proposition, that proposition is also intuitively true. This justifies the use of transfinite mathematics: it is not only internally consistent, but it proves only true intuitive propositions (and indeed all, since a formalization of intuitive mathematics is part of the formalization of all mathematics).

        In 1926, Hilbert introduced a distinction between real and ideal formulas. This distinction was not present in 1922b and only hinted at in 1923. In the latter, Hilbert presents first a formal system of quantifier-free number theory about which he says that “The provable formulae we acquire in this way all have the character of the finite”

        In other words, Hilbert does not require assigning any sense of truth beyond the symbolic one to those mathematical statements that do not correspond to physical reality, but those statements that can correspond to physical reality (i.e. the "real formulas") must do so, and those "real formulas" are meaningfully true beyond the symbols.

        The earlier formalism (mathematics is just symbols) could no longer be justified after Gödel, as consistency was its main justification.

        If anything, I think it's constructivism that suffers from a philosophical issue in requiring meaning that isn't physically realisable -- unlike ultrafinitism, for example. Personally, I find both Hilbert's formalism and ultrafinitism more philosophically satisfying than constructivism, as they're both rooted in physical reality, whereas constructivism is based on "computation in principle" (but not in practice!).

        > As for what most people think about the philosophical implications, nobody should be expected to have any meaningful philosophical opinions about topics that they have not yet tried to think about

        I mean people who have thought about it.

        [1]: https://plato.stanford.edu/entries/hilbert-program/

        Reply View 9 replies
  • woolion 5 days 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.

    Reply View 4 replies
    • btilly 5 days 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.

      Reply View 3 replies
      • bubblyworld 4 days ago

        Mmm, the problem with computable foundations (in my opinion anyway) is that it takes a lot of stuff that is trivial in standard foundations (equivalence relations, basic operations of arithmetic and their laws, quotients, etc) and fills them with subtle logical footguns.

        As you say, some view this as a feature, not a flaw. But to my mind mathematics is a tool for dissecting problems with hard formal properties, and for that I'd like the sharpest scalpel I can find.

        For me classical foundations strikes a good balance between ease of use and subtlety of reasoning required to get results. I'm not sure the non-constructive and self-referential bits bother me, they don't really get in the way unless you're studying logic (in which case you're interested in computability and other foundations anyway).

        Reply View 2 replies
  • IsTom 4 days ago

    > In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size?

    The way I see it is that an existence of proof isn't required for something to be true. Something being true is a matter of the model, being provable is a matter of axioms and deduction rules. And there comes the distinction between ⊨ and ⊢.

    Reply View 0 replies