Hacker News Reader

Yeah, it's important to think of these axioms as choosing the rules of the game, rather than what intuitively makes sense. The real question is if playing the game produces useful results.

Spoken like a true formalist.

It doesn't really have to mean anything when we say that the reals are a larger set than the natural numbers - that's just the conclusion of the game that we are playing.

What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?

> What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?

The claim that there are more reals than naturals holds given classical ZF(C) set theory. But there are alternative set theories in which the reals are countable, e.g. NFU+AxCount. These alternative set theories ensure all reals are countable by rendering Cantor’s diagonalisation argument invalid, since their axioms are too weak to validate it. But, they contain all the same reals as the high school mathematics concept of “reals”. So, there are many reals, and that some of them are countable and others are not are indeed “eternal truths” (it is an eternal truth that whatever axioms have the consequences they do), but the everyday (non-expert) concept of reals isn’t any of them in particular - and it is unclear if the dominance of classical notions in mainstream professional mathematics was historically inevitable or a historical accident - maybe, on the other side of the galaxy, there exists some alien civilisation, in which different foundations of mathematics are mainstream, because their mathematics took a different evolutionary course from ours - maybe for them, reals are classically countable, and uncountability is an exotic notion belonging to alternative foundations of mathematics

As I pointed out at https://news.ycombinator.com/item?id=44271589, there are systems that can accept Cantor's argument, without concluding that there are more reals than rational numbers.

As you point out, there are many mathematical systems that contain all of the numbers in the high school mathematics concept of "reals". Since those with a high school understanding of reals do not know which of those systems they would agree with, they should not be asked to accept as true, any results that hold in only some of those systems.

And that is why I don't like mathematicians telling lay audiences that there are more reals than rationals.

"Cantor's diagonalization argument" is best understood as a mere special case of Lawvere's fixed-point theorem. Lawvere's theorem is really the meat of the argument, and it's also the part that is very easy for exotic systems to "accept", since it's close to a purely logical argument. Whether these systems truly accept "Cantor's argument" is perhaps only a matter of perception and intuition, that people may perhaps disagree about.

It does not matter what your best understanding of Cantor's diagonalization argument is. In some mathematical systems it means, "there are more reals than natural numbers", and in others it means, "the reals encode self-reference in a more direct way than the natural numbers do".

The result is that it is possible for the acceptance of the argument to lead to very different consequences about what we then conclude.

> "Cantor's diagonalization argument" is best understood as a mere special case of Lawvere's fixed-point theorem. Lawvere's theorem is really the meat of the argument, and it's also the part that is very easy for exotic systems to "accept", since it's close to a purely logical argument.

Okay, but can you prove Lawvere’s theorem in NFU+AxCount?

And even if you can, since NFU+AxCount proves that the reals are countable, if NFU+AxCount proves Lawvere, then (to echo what btilly says in a sibling comment) NFU+AxCount+Lawvere couldn’t entail the countability of the reals, since that would render NFU+AxCount trivially inconsistent, and we know it is isn’t trivially inconsistent (as with any formal system, consistency is ultimately unprovable, but if a system is taken seriously as an object of mathematical research, then any inconsistency must be highly non-trivial.)

I agree, but I also want to clarify that cantors argument was about subsets of the naturals (N), or more precisely functions from N to Bool (the decidable subsets). This is where the diagonal argument makes sense.

So to conclude that there are more reals than naturals, the classical mathematical argument is:

a) There are more functions N to Bool than naturals.

b) There are as many reals as functions from N to Bool.

Now, we of course agree the mistake is in b) not in a).

> So to conclude that there are more reals than naturals, the classical mathematical argument is:

> a) There are more functions N to Bool than naturals.

> b) There are as many reals as functions from N to Bool.

> Now, we of course agree the mistake is in b) not in a).

Given certain foundations, (a) is false. For example, in the Russian constructivist school (as in Andrey Markov Jr), functions only exist if they are computable, and there are only countably many computable functions from N to Bool. More generally, viewing functions as sets, if you sufficiently restrict the axiom schema of separation/specification, then only countably many sets encoding functions N-to-Bool exist, rendering (a) false

Indeed, what you write is true from an external point of view; just note that within this flavor of constructive mathematics, the set of functions from N to Bool is uncountable again.

There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.

Is it internally uncountable in the strong sense that the system can actually prove the theorem “this set is uncountable”, or only in the weaker sense that it can’t prove the theorem “this set is countable”, but can’t prove its negation either?

If the latter, what happens if you add to it the (admittedly non-constructive) axiom that the set in question is countable?

It should be true in the stronger sense.

Suppose that you've written down a function enumerate, that maps all natural numbers to functions that themselves map all natural numbers to booleans. We then can write down the following program.

    (defn unenumerated (n) (not ((enumerate n) n)))

This function can be recognized as Cantor diagonalization, written out as a program.

If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.

This argument is, of course, just Cantor's diagonalization argument. From an enumeration, it produces something that can't be in that enumeration.

> If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.

Okay, but if we take the position that only non-halting (for all inputs) programs represent functions over N, if your program “unenumerated” never halts for some N, it doesn’t represent a function, so your argument isn’t a case of “using the enumeration of all functions to produce something which doesn’t belong to the enumeration”

Obviously an enumeration of all computable functions isn’t itself computable. But if we consider Axiom CompFunc “if a function over N is computable then it exists” (so this axiom guarantees the existence of all computable functions, but is silent on whether any non-computable functions exist) and then we consider the additional Axiom CountReals “there exists a function from N to all functions over N”, then are those two axioms mutually inconsistent? I don’t think your argument, as given, directly addresses this question

It's just a straight up liar's paradox. If enumerate is a function that works as advertised, then unenumerated is as well. If enumerate tries to list unenumerated, then enumerate can't work as advertised.

For the argument that I gave to work, you need what you might call Axiom ComposeFunc, you may always compose a new function by taking an existing function and doing something that is known to be valid with it. Obviously this axiom is true about the computable universe. But, more than that, it is also true about any generalization of "function" that behaves like most would expect a function to have.

Now it is true that your Axiom CompFunc and Axiom CountReals do not necessarily contradict each other. But CompFunc, ComposeFunc and CountReals do contradict each other, and the contradiction can be built by following Cantor's diagonalization argument.

> But, more than that, it is also true about any generalization of "function" that behaves like most would expect a function to have.

It isn’t true in NFU though, correct? At least not in the general case. Because Cantor’s argument fails in NFU

If I understand what I just Googled correctly (definitely not guaranteed), the reason why Cantor's argument can fail in NFU is that NFU does not necessarily allow you to build a function that returns things in X, out of a function that returns functions returning things in X.

So it has non-computable functions, but also has a type system that tries to avoid allowing self-reference. And that type system gets in the way of Cantor's argument.

I clearly hadn't thought of this possibility. It is a constraint of a kind that doesn't show up in the computable universe.

And so, going back, if the the Russian constructivist school does indeed center on computability, then my first answer to you was correct.

Right, I think we are in agreement - a pure Russian constructivist approach which only permits computable functions cannot prove the reals are countable. However, I still am sceptical it can prove they are uncountable-if you limit yourself to computable constructions, you can’t actually computably construct a Cantor diagonal, so his argument fails just like it does in NFU.

The (un)countability of the reals is known to be independent of NFU-it is consistent both with the reals being countable and them being uncountable. There are two different axioms which it is standard to add to NFU to decide this-AxCount≤ which implies the reals are countable and AxCount≥ which implies the reals are uncountable.

I guess I was suggesting that in the same way, an additional axiom could be added to computable set theory which renders the reals countable or uncountable. If an additional axiom asserting the countability of the reals involves the existence of a function from the naturals to functions over the naturals, that would obviously be introducing an uncomputable function-but for that to produce an inconsistency, it would need to enable Cantor’s argument-and, given your “ComposeFunc” in the computable universe is already restricted to only operating over computable functions, it is reasonable to limit its application to computable functions in an extension, which would mean the addition of this uncomputable function would still not permit Cantor’s argument

There is nothing uncomputable with the cantor diagonalisation. The Russians gladly accept it, I assure you. Here is a Haskell implementation:

diag :: (nat -> (nat -> Bool)) -> (nat -> Bool)

diag f n = not (f n n)

The following argument is also constructive. Just like in classical mathematics, crustructive mathematics proves the negation of A by assuming A and deriving a contradiction. (But you cannot prove A by assuming it’s negation and deriving a contraction):

Assume a surjectiom f :: nat -> Bool. Then there is x such that f x = diag f. Since these two functions are equal, they take equal values when we evaluate them in any point. In particular f x x = diag f x, but since diag f x = not (f x x), by definition, we have that f x x = not (f x x). This is a contradiction since not does not have fixed points.

( I made nat a type variable here since this works for any type / set )

Bringing in computability from an external point of view is a mistake here. Markov had no issue with a. He would only disagree with b.

> Spoken like a true formalist.

Doesn't seem to be a bad thing. There are some famous cranks who reject the concept of infinity, since I suppose they have problems wrapping their head around it.

> What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?

People misunderstand mathematics all the time. It's ok, it's part of the journey.

Axioms are also introduced in practical terms just to make proofs and results "better". Usually we talk in terms of what propositions are provable, saying that indicates the strength/power of these assumptions, but beyond this there are issues of proof length and complexity.

For example in arithmetic without induction, roughly, theorems remain the same (those which can still be expressed) but may have exponentially longer proofs because of the loss of those `∀n P(n)`-type propositions.

In this sense it does sometimes come back to intuition. If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition and doesn't really change "the game" we are trying to play. It just makes it more intuitive and playable.

Good point. I would argue, however, that having nicer proofs is a "useful" result of the game.

I’m not sure what you mean by “theorems remain the same”. If you take away induction from Peano arithmetic, you get Robinson arithmetic, which has many more models, including (from https://math.stackexchange.com/a/4076545):

- ℕ ∪ {∞}

- Cardinal arithmetic

- ℤ[x]⁺

Obviously, not all theorems that are true for the natural numbers are true for cardinals, so it seems misleading to say that theorems remain the same. I also believe that the addition of induction increases the consistency strength of the theory, so it’s not “just” a matter of expressing the theorems in a different way.

I would agree more for axioms that don’t affect consistency strength, like foundation or choice (over the rest of the ZF axioms).

If I had to write again I might say "same theorems about natural numbers" and capitalize ROUGHLY. It is a conversation, what exactly I am weaseling around (not just nonstandard model theoretic issues), and I take your caveat about consistency strength - with that said would you still call it misleading? Why is it that eg x+y=y+x for x y given takes exponential length proof in Robinson compared to PA? For the reason stated, which is true in a very broad sense.

> If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition

But how can you prove that P(n) for all n without induction? Maybe I misinterpret what you're saying, or I'm naive about something in formal languages, but if we can prove P(n) for all n. then `∀n P(n)` just looks like a trivial transcription of the conclusion into different symbols.

I think the crux of the matter is that we accept inductive arguments as valid, and so we formalize it via the inductive axiom (of Peano arithmetic). i.e., we accept induction as a principle of mathematical reasoning, but we can't derive it from something else so we postualte it when we come around to doing formalizations. Maybe that's what you mean by it coming down to intuition, now that I reread it...

Poincaré has a nice discussion of induction in "On the nature of mathematical reasoning", reprinted in Benacerraf & Putnam Philosophy of Mathematics, where he explicates it as an infinite sequence of modus ponens steps, but irreducible to any more basic logical rule like the principle of (non-)contradiction

Rejecting induction could be quite useful if you want to be very precise about the implications of your constructions wrt. computational complexity. This is of course only a mildly strengthened variant of the usual arguments for constructivism.

> But how can you prove that P(n) for all n without induction? Maybe I misinterpret what you're saying, or I'm naive about something in formal languages, but if we can prove P(n) for all n. then `∀n P(n)` just looks like a trivial transcription of the conclusion into different symbols.

Of course it is likely that an interesting result about all positive integers, that is "really" about positive integers, is proved by induction, but you certainly don't need induction to prove P(n): n = 1.n, or, more boringly, P(n): 0 = 0. (These statements are obviously un-interesting, both in the human sense of the word and in the sense that they are just statements about semi-rings, of which the non-negative integers are an example.)

My understanding is that the difference between "For every positive integer n, I can prove P(n)" and "I can prove ∀n.P(n)" is that the former only guarantees that we can come up with some terrible ad hoc proof for P(1), some different terrible ad hoc proof for P(2), and so on. How could I be sure I have all these infinitely many different terrible ad hoc proofs without induction? I dunno, but that's all that the first statement guarantees. Whereas the second statement, in the context of computability, guarantees that there is some computable function that takes a positive integer n and produces a proof of P(n); that is, there is some sort of guaranteed uniformity to the proofs.

I think it may be easier to picture if connected with math_comment_21's analogy in https://news.ycombinator.com/item?id=44269153: the analogous statements in the category of topological spaces (I think one actually has to work about topos, but I don't know enough about topos theory to speak in that language) about a map f : X \to Y are "every element of Y has a pre-image under f in X" versus "I can continuously select, for each element of Y, a pre-image of it under f in X", i.e., "there is a continuous pre-inverse g : Y \to X of f."

>> If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition

> But how can you prove that P(n) for all n without induction?

Just to be clear to all readers, the axiom of COUNTABLE choice is uncontroversial. Nobody is disturbed by induction.

The issue it that when you allow UNCOUNTABLE choice - choices being made for all real numbers (in a non-algorithmic way, I believe - so not a simple formula) - there are some unpleasant consequences.

How is it different from using ZF as a meta-theory to study ZF(C)? Is there anything special about category theory vis-à-vis ZF as a meta-theory? You're not arguing about ontology or the nature of truth, because you've picked category theory as your ontology just like you could pick ZF or ZFC.

Category theory gives a structural framework for discussing these things. The various categories live side by side and can be related with functors. This allows a broader view and makes it easier perhaps, to understand that there isn’t a right answer to “what is true” about sets in the absolute.

But then you would think there is a right answer to “what is true” about categories, and you would face AC again.

For sure there would have to be a meta theory of some sort. But, I think that many classical mathematicians would be happy with that meta theory to be weaker, rather than stronger. I don't think there is a need for that theory to have AC. After all, thanks to its independence of from the other axioms, AC does not add logical strength to a classical theory.

(For die-hard constructivists, such as myself, the story is of course different. But that story is for a another time. I am presenting the classical view here.)

Doesn't "continuous" make all the difference here? AC doesn't contain a comparable limitation, so the analogy doesn't work that week.

Careful here, you might wake up the diabol (of pure algebra)

Yes, but the parent comment is trying to say "imagine the world would only be made up of topological spaces and continuous maps". Then the retraction principle would not hold.