Here's a breakdown of the themes discussed in the Hacker News thread, with supporting quotes:
The Axiom of Choice and Mathematical Frameworks
The discussion revolves around the implications of accepting or rejecting the axiom of choice, and the broader idea that mathematical axioms are choices that define the "rules of the game." This choice impacts which theorems can be proven and the nature of mathematical "truth."
-
Axioms as Rules: "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." (karmakurtisaani)
-
Alternative Set Theories: "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." (skissane)
-
Flexibility in Mathematical Systems: "[...]there's this category, Set, with this rule, and there's this other category called idk Snet, that satisfies the ZF axioms but where there are some surjections that don't split, and that's ok too." (math_comment_21)
The Uncountability of Reals and its Interpretation
A significant portion of the conversation focuses on Cantor's diagonal argument and the implications of the uncountability of the reals. The discussion questions how universally this concept is understood and whether it is an "eternal verity." Alternative interpretations and the role of foundational systems are also examined.
-
Questioning Universal Acceptance: "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?" (btilly)
-
Systems Accepting Cantor's Argument Without Uncountability: "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." (btilly)
-
Cantor's Argument and Lawvere's Fixed-Point Theorem: ""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." (zozbot234)
-
Alternative Interpretations of Cantor's Argument: "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'." (btilly)
-
Underlying mistake in proving reals are uncountable: "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)." (gylterud)
-
Disagreement in classical mathematical argument: "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" (skissane)
Constructivism and Computability
The discussion touches upon constructivist mathematics, where the existence of mathematical objects requires a construction method. This leads to a discussion of computable functions and their role in determining the countability of the reals.
-
Computable Functions and the Russian Constructivist School: "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." (skissane)
-
Internal vs. External Uncountability: "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." (IngoBlechschmid)
-
Liar's Paradox and ComposeFunc Axiom: "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." (btilly)
The Role of Axioms in Proof and Intuition
The conversation also considers why certain axioms are chosen and how they impact the ease and "niceness" of proofs aside from consistency strength of provable theorems.
-
Intuition and Acceptance of Axioms: "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." (woopsn) -
Axioms for Better Proofs: "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." (woopsn)
-
Niceness of Proofs Considered 'Useful': "Good point. I would argue, however, that having nicer proofs is a 'useful' result of the game." (karmakurtisaani)
Induction and Its Justification
The thread includes a discussion on the necessity of induction and how it is perceived as a fundamental principle, rather than something derived.
-
Induction as an Accepted Principle: "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." (griffzhowl)
-
Rejecting Induction can refine Computational Complexity. "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". (zozbot234)