Comment by mietek

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

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.

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.

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!

> 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?)

> 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.