Comment by btilly

Comment by btilly 5 days ago

35 replies

View on Hacker News

I wish that I had specific suggestions.

My overall wish that more people understood why, in intuitionist mathematics, uncountable means "self-referential" and not "more". No infinite set can have "more" elements than any other, because all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist.

(By internet coincidence, I recently wrote https://math.stackexchange.com/questions/5074503/can-pa-prov... which ends with the beginning of the construction of that list, starting with the Peano axioms. https://news.ycombinator.com/item?id=44269822 is about that answer.)

Of course Formalists simply write down some axioms, start constructing proofs, and don't worry about what it really means. In what sense do uncountable hordes of real numbers that can never be specified in any way, truly exist? It doesn't matter. These are the axioms that we chose, and that is the statement that we came up with.

I have no idea of whether there is a way to formalize or prove the following idea. If there is, it would be good to mechanize it.

All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth.

Jtsummers 5 days ago

A nit, but:

> Strictly speaking, a programming language doesn't really need comments. "But Lisp has them, and puts them in double quotes."

Lisp has comments, but they aren't generally contained in double quotes, you've tossed a lot of strings into your program and called them comments. Comments are either marked with ; (comment to end of line, like //) with conventions on how many semicolons to use in particular places, or comment blocks with #| comment |# (nestable version of /* */). You can add documentation to many definitions, like functions, using strings which may be what you're thinking of but that happens inside the definition like with this:

  (defun constant (x)
    "CONSTANT returns a function which always returns X"
    (lambda (a) x))
Which is a comment, but it's unusual to use strings as comments outside of contexts like that. Also, if you're going to use strings as comments you can make them multi-line instead of doing

  "I thought about calling these car and cdr..."
  "...then decided that I'm not really THAT addicted to Lisp"
with:

  "I thought about calling these car and cdr...
  ...then decided that I'm not really THAT addicted to Lisp"
The other reason I'm posting this nit is that if anyone reads your blog/answer and tries to use comments as you've described them inside of expressions they'll be very confused about why it's behaving incorrectly. There's no reason to mislead people, this is not a comment:

  (if (= 1 2) "Should never be true" ;; that's not a comment, it's an expression
    (print "Never happens")
    (print "Always happens")) ;; your interpreter or compiler will complain about this code
Reply View 1 reply
  • btilly 5 days ago

    Thank you, fixed.

    And that is why I did think that. I only play with the ideas of Lisp. I've never really had to use it. So I looked at a Lisp example, saw something that looked like it was functioning as a comment, then used that comment style.

    Reply View 0 replies
SabrinaJewson 5 days ago

Relevant to this is Skolem’s paradox (https://en.wikipedia.org/wiki/Skolem%27s_paradox), which states that any uncountable set can be modelled by a countable set.

In that light, the statement that the reals have greater cardinality than the naturals can be thought of as a statement that _our model of set theory_ happens to contain no injections from the reals to the naturals. Not that they can’t exist in a Platonic sense, or even just in the metatheory.

Reply View 1 reply
  • btilly 5 days ago

    That does seem extremely relevant. And is a mirror of the fundamental insight behind nonstandard analysis. Which is that that any set containing the integers that follows some set of axioms, has a nonstandard model that follows a nonstandard version of those axioms, and which contains infinite integers.

    This can be seen as why it is different for a set of axioms to prove that it proves something, than it is to prove something directly. Because when the axioms prove that they prove, you might be in a nonstandard model where that "proof" is infinitely long, and therefore isn't really a proof!

    And that is why, for example, if PA is consistent, then it remains consistent if you extend PA with the axiom, "PA is not consistent". Clearly any model of that extended set of axioms does not describe what we want PA to mean. But that doesn't mean that it logically contradicts itself, either.

    Reply View 0 replies
woolion 5 days ago

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.

Reply View 24 replies
  • 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

        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
    • 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
    • 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
practal 4 days ago

Gödel's incompleteness theorem tells you why it is a good idea to separate semantics (notion of truth) from syntax (reasoning). Because some things are true, although you cannot prove that they are.

Some people now put forward from this the idea that for the natural numbers we know, it is NOT either true or false if for example the twin prime conjecture holds. That is nonsense. It is just that our methods of proof are strictly weaker than our notion of truth is.

That this is so is not even surprising! It is a fact of life that what is true is not necessarily what you can prove to be true. Innocent people imprisoned are an example of that. Guilty people going free another. What is maybe surprising is that what is true in what we perceive as the "real world" is also true in mathematics, which we imagine to be an "ideal realm". But mathematics is ALSO part of the "real world"; if you understand this, it is not so surprising. Yes, I am a platonist, and I think that everybody who isn't is just plain wrong and confused.

Intensional functions are just a special case of extensional functions. Where extensional functions are defined on mathematical objects, intensional functions are extensional functions defined on representations of mathematical objects (which are also mathematical objects, by the way), but pretend to be acting on the mathematical objects themselves, not their representations. That is really all there is to it, it is not a deep philosophical mystery. To do so can of course be very useful!

Reply View 0 replies
cvoss 5 days ago

> there is a single countable list that includes all things that might possibly have any mathematical existence at all.

Help me understand that. Isn't the Cantor diagonialization argument a proof that such a list cannot exist because, supposing it did exist, it could be used to construct an object not on the list? Are you proposing that your list somehow defeats Cantor here?

(Of course, we're using the word "list" loosely here. What we mean is a total function with domain Nat, right?)

Reply View 1 reply
layer8 5 days ago

> all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist.

The universe (in the cosmological sense) can be written down as a single countable list, and anything different would be impossible? Or are you saying that it does not truly exist? I’m not sure how that makes sense.

Reply View 2 replies
  • btilly 5 days ago

    We can create a countable list that contains every possible description that can ever be created. For example just write down numbers in base ASCII, using a programmable markup language (like TeX) that lets us represent anything that we want. (OK, TeX can only describe shapes down to the wavelength of visible light, but that's good enough for me.)

    In what sense does an idea exist when it cannot be described by anything on that list?

    Reply View 1 reply
    • layer8 5 days ago

      To quote an old adage, the map isn’t the territory. That we can’t fully write it down (which we can’t even for countable infinities, or even something like 10^10^10 symbols) doesn’t mean that it doesn’t exist. All of the territory still exists, even if any map that we can draw will only capture certain aspects of it.

      Regarding “ideas”, to me math is primarily exploration and discovery, rather than invention. That’s one way how it corresponds to the territory analogy.

      Reply View 0 replies