In topology, if you have a continuous surjective map X --> Y, then it might have a continuous splitting (a map the other way which is a "partial" inverse in the sense that Y ---> X ---> Y is the identity) e.g. there are lots of splittings of the projection R^2 ---> R, you could include the line back as the x-axis but also the graph of any continuous function is a splitting.
On the other hand, there's no continuous splitting of the map from the unit interval to the circle that glues together the two endpoints.
So the category of topological spaces does not have the property "every epimorphism splits."
As the article mentions, the axiom of choice says that the category of sets has this property.
So we can think of the various independence results of the 20th century as saying, hey, (assuming ZFC is consistent) 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.
Then whatever, if you want to study something like rings but you don't like the axiom of choice, define a rning to be a snet with two binary operations such that blah blah blah, and you've got a nice category Rning and your various theorems about rnings and maybe they don't all have maximal ideals, even though rings do. You're not arguing about ontology or the nature of truth, you're just picking which category to work in.
karmakurtisaani · 15h ago
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.
woopsn · 12h ago
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.
SabrinaJewson · 10h ago
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).
woopsn · 7h ago
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.
griffzhowl · 8h ago
> 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
fn-mote · 5h ago
>> 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.
zozbot234 · 8h ago
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.
JadeNB · 6h ago
> 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."
karmakurtisaani · 10h ago
Good point. I would argue, however, that having nicer proofs is a "useful" result of the game.
btilly · 13h ago
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?
skissane · 10h ago
> 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
btilly · 10h ago
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.
zozbot234 · 10h ago
"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.
btilly · 10h ago
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.
skissane · 10h ago
> "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.)
gylterud · 9h ago
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).
skissane · 9h ago
> 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
IngoBlechschmid · 7h ago
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.
skissane · 5h ago
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?
btilly · 5h ago
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.
skissane · 4h ago
> 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
btilly · 2h ago
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.
skissane · 2h ago
> 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
btilly · 2h ago
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.
skissane · 11m ago
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 “CompFunc” 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
karmakurtisaani · 10h ago
> 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.
LudwigNagasena · 9h ago
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.
gylterud · 9h ago
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.
alexey-salmin · 10h ago
Doesn't "continuous" make all the difference here? AC doesn't contain a comparable limitation, so the analogy doesn't work that week.
gsf_emergency · 5h ago
Careful here, you might wake up the diabol (of pure algebra)
mietek · 15h ago
Author of the mechanization here. Feel free to suggest materials from the history of intuitionistic mathematics and type theory that ought to be mechanized and made available to a wider audience — the less well-known, the better.
btilly · 13h ago
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.
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 · 13h 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
btilly · 13h 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.
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.
btilly · 12h 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.
woolion · 12h 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.
btilly · 12h 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.
pron · 11h 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.
zozbot234 · 10h 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.
btilly · 9h 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.)
zozbot234 · 8h 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.
btilly · 10h 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.
pron · 10h 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 was responding to this statement of yours, "I don't think that humans philosophically reject non-constructive results."
Some of the humans who have thought about it do reject them. Some of the humans who have thought about it don't reject them.
Most humans, including most mathematicians, have never truly thought about it.
pron · 9h ago
> Some of the humans who have thought about it do reject them.
I think they reject them only if they misrepresent Hilbert's formalism, because formalism does not assign them any meaning of truth beyond the symbolic. It makes no statement that could be rejected: a mathematical theorem that proves a set "exists" does not necessarily make any claim about its "actual" existence (unlike, say, Platonism). You asked in what sense does such a set exist, and Hilbert would say, great question, which is why I don't claim there necessarily is any such sense.
What those who reject Hilbert's formalism reject is the validity of a system of mathematics where only some but not all propositions are "externally" meaningful, but such a rejection, I think, can only be on aesthetic grounds, because, again, for Hilbert, all "valid" foundations must agree with physical reality when it comes to statements that could be assigned physical meaning. If ZFC led to any result that doesn't agree with physical reality, Hilbert would reject it, too. But it hasn't yet.
btilly · 8h ago
I believe that you are misrepresenting Hilbert here.
If ZFC led to a result that doesn't agree with physical reality, Hilbert would not reject that result. Instead, at worst, he would simply move it from the category of being a real formula, to being an ideal formula. For example, Euclid's geometry doesn't agree with physical reality. Therefore it is an ideal formula, not a real formula. And yet we do not reject this geometry from mathematics.
But the distinction between real and ideal is a question for physics. It is not a question that mathematicians need worry about. The questions that mathematicians need worry about are entirely those which are internal to the formal game.
pron · 7h ago
> Instead, at worst, he would simply move it from the category of being a real formula, to being an ideal formula.
No. No result, either ideal or real, may contradict reality (it's just that since infinitary statements do not describe reality, they obviously cannot contradict it). You can think about it like this: According to Hilbert, a valid mathematical foundation is any logical theory that is a conservative extension of reality. ZFC, constructive foundations, and ultrafinitist foundations all satisfy that, so they would all be valid foundations according to that principle.
> For example, Euclid's geometry doesn't agree with physical reality.
It may not describe physical reality, but it doesn't contradict it.
> But the distinction between real and ideal is a question for physics. It is not a question that mathematicians need worry about. The questions that mathematicians need worry about are entirely those which are internal to the formal game.
Not only does that disagree with Hilbert's formalism, it also disagrees with constructivism. The question of the philosophy of mathematics is precisely what, if anything, does mathematics describe beyond symbols.
btilly · 5h ago
I have absolutely no idea how physical reality can contradict a statement about a formal symbol game.
I am also convinced that what you are saying is not what Hilbert actually meant.
But he died before I was born, so I can't ask him. Besides, I don't speak German.
tsimionescu · 1h ago
I think what the poster above means is that any formal system in which, say, 1 + 1 = 75, even if internally consistent as a set of symbols, would not be considered a valid logical foundation for mathematics by Hilbert, because it directly contradicts physical reality. Of course, this is under the assumption that 1 and + and 75 are meant to have their usual meanings, not that we've redefined the + operator to mean "the 73rd successor", nor that we're operating in some exotic numerical base where 75 is just a different set of symbols to describe the number 2.
IsTom · 8h 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 ⊢.
woolion · 11h 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.
btilly · 11h 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.
bubblyworld · 1h 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).
cvoss · 10h 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?)
> 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.
btilly · 10h 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?
layer8 · 10h 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.
franklin_p_dyer · 13h ago
Really cool post! This is an awesome idea and I'd love to see more of these. :-)
Maybe these won't be the kind of thing you are looking for, but here are some gems that would be cool to see formalized, some of which I've been meaning to do myself someday:
- There are many parts of the book "A Course in Constructive Algebra" (Mines, Richman, Ruitenburg) worthy of being formalized, but even just the discussion of "omniscience principles" in the first chapter would be cool.
- I absolutely love Sierpinski's book "Cardinal and Ordinal Numbers", and although I'm not sure it would be considered a book of "intuitionistic mathematics", he is careful enough about pointing out where he uses AoC for parts of his book to be suitable for consideration. The results and exercises in VI.5 "Axiom of choice for finite sets" are probably my favorite in the whole book and would be awesome to see formalized.
- I am not sure about a historical article/source for this one, but formalization of some results about Dedekind-finite and Dedekind-infinite sets (https://en.wikipedia.org/wiki/Dedekind-infinite_set) could be really fun. I find these to be very counterintuitive.
So if I understand the claim of this correctly (I'm a spectator of logic research and haven't tried to follow the proofs), there is a constructive version of AoC that is obviously true, but it's not the same as Zermelo's axiom because that one is extensional. Zermelo's axiom can be formulated in constructive mathematics but gives you things you don't want (like excluded middle.)
Is this close to a correct statement of the paper's result? Is all this agreed on today? Have there been any significant refinements?
ncfavier · 14h ago
That sounds about correct. The naïve interpretation of AC that interprets ∃ as Σ and ∀ as Π amounts to the trivial fact that Π distributes over Σ, which has little to do with any choice principle. If you instead interpret it in setoids, as Martin-Löf does, then the function you get should be extensional with respect to the relevant setoid structures, which is where the power of the axiom comes from.
The modern view on this is homotopy type theory, where types themselves are intrinsically seen as ∞-groupoids (a higher analogue of setoids) and ∃ is interpreted as a propositionally truncated Σ-type (see chapter 3 of the HoTT book). In this setting the axiom of choice says that for any set X, (∀ (x : X). ∥ P x ∥) → ∥ ∀ (x : X). P x ∥ (see section 3.8).
Note that from the perspective of homotopy type theory, Zermelo's axiom of choice is too strong: it is equivalent to global choice (for all types A, ∥ A ∥ → A), which is inconsistent with univalence.
creata · 12h ago
Off-topic: What's the state of homotopy type theory as an alternative foundation for mathematics? Has it been used to simplify any proofs or prove anything new?
zozbot234 · 10h ago
Kevin Buzzard (a standard mathematician who has direct expertise in the sorts of things HoTT is supposed to help with) argues that we simply don't know yet. See the references I previously mentioned in https://news.ycombinator.com/item?id=44151283
YetAnotherNick · 4h ago
In podcasts or open conversation he is far more critical of HoTT.
jfengel · 9h ago
There's no problem. It's obviously true. Just like the well ordering principle is obviously false.
(To explain the joke: they are equivalent, but they strike the intuition very differently.)
CliffStoll · 13h ago
And the Axiom of Choice implies the Banach-Tarski parodox.
It's anti-intuitive:
Disassemble a pea into a finite number of pieces. Then reassemble those pieces to create the sun.
nwallin · 7h ago
> Disassemble a pea into a finite number of pieces. Then reassemble those pieces to create the sun.
"Finite number of pieces" is a tricky thing. It's a finite number of pieces, sure, but each of those pieces is made of an uncountably infinite number of pieces. Banach-Tarski is a clever way of sweeping an infinite number of dust bunnies under the rug until just the right moment, when it reveals all infinitely many of them in the shape of a pea and claims to have just created them, when in reality, they were actually there all along, hiding under the rug.
For me, Banach-Tarski is just an another version of Hilbert's Hotel, but with uncountable infinities instead of countable ones. Once you accept, in your heart, that infinity is real and is equally deserving of your love and respect as finite natural numbers, then the paradoxicalness of Banach-Tarski melts away.
fpoling · 5h ago
Essentially the axiom of choice allows for 3-d sets that do not preserve their volume upon rotation/movement.
Such sets, of cause, cannot be constructed or even described as their description will contain infinite number of steps.
tweakimp · 9h ago
Can you really reassemble them into something bigger or just into more copies of the same size?
dist-epoch · 12h ago
The number of pieces is finite, but each piece consists of an infinite number of scattered points:
> However, the pieces themselves are not "solids" in the traditional sense, but infinite scatterings of points.
scoofy · 14h ago
Axioms are arbitrary. Use them if they are useful.
ptero · 14h ago
Axioms should capture the rules we can assume without justification.
But in most cases we want them to reflect the rules of the real world in the sense that statements derived from those axioms reflect our observations. That part (reflect observations) can be separated by many levels of abstractions, etc. I would not try visualizing general statements on Lie algebras or spectral theorems, but those abstractions serve the same goal -- help derive conclusions that apply in the real world. My 2c.
simion314 · 14h ago
It is not about real world, choosing an axiom set must simply put produce something valid (with no contradictions) and that is not trivial.
ptero · 11h ago
Some math is not about the real world. This is not my kettle of fish, but I have heard of some general topology research directions that discusses properties of topological spaces that probably do not exist at all. Those (according to a friend whose advisor worked in the area) are pretty sad affairs, with only 5-10 people in the world who understand or care about this particular sliver of the math.
But some math is about providing tools (again, likely via levels of abstractions) for understanding the world and, to me, this is the "real math".
This is a personal view, not an absolute position. I started on the other side of this fence and during my pure math PhD regularly picked fights with our buddies doing physics PhD arguing that mathematics is self-sufficient and does not need any validation from other sciences. But over the next 30 years gradually went to the other side and now think that my original view leads to splintering into gazillion tiny slivers that do not care about anything else; not even about adjacent slivers. Which leads to degeneration. My 2c.
dist-epoch · 12h ago
Math is done backwards.
We know what kind of results we want to be true, and then we search for the minimum number of axioms which can deliver that.
woopsn · 11h ago
There is another goal in addition to minimizing the number/complexity of axioms. Some "axioms" like induction actually introduce an infinite family of assumptions, a so-called schema. So in addition to working backwards from our (incomplete) knowledge, we find certain axioms let us make arguments that are obviously valid but would be formally very tedious without them.
impostervt · 15h ago
I've never quite gotten the axiom of choice. Can anyone ELI5?
bobbylarrybobby · 14h ago
The Cartesian product of nonempty sets is nonempty.
This is obvious!, you might say — obviously we can just pick one element from each set and be done with it. But the statement that we can pick an element from each set is the axiom of choice.
Note that it's not necessarily simple to pick an element from a set. For instance, how would one pick an element from the set of uncomputable numbers? A human cannot describe said element, by definition. The axiom of choice says it's possible anyway.
SabrinaJewson · 14h ago
> The Cartesian product of nonempty sets is nonempty.
>
> This is obvious!, you might say — obviously we can just pick one element from each set and be done with it. But the statement that we can pick an element from each set is the axiom of choice.
No? I don’t see how this relates to AC at all. AC is about making an infinite number of choices at once – if you’re just making two choices (or, more generally any finite number of choices), as is needed here to prove that this Cartesian product is nonempty, then that’s completely fine without extra axioms. See for example https://mathoverflow.net/q/32538
E.g. in type theory, one term of type `Nonempty(A) → Nonempty(B) → Nonempty(A × B)` (supposing that `Nonempty` is defined as the [bracket type](https://ncatlab.org/nlab/show/bracket+type)) would just be `λ [a] ↦ λ [b] ↦ [(a, b)]`.
gjm11 · 12h ago
What AC's equivalent to is "the Cartesian product of any set of nonempty sets is nonempty". Not just of two nonempty sets, for which indeed you don't need AC.
Kranar · 11h ago
The two statements imply each other, they are logically equivalent:
>One of many ways to express the axiom of choice is to say that it is equivalent to the statement that the Cartesian product of a collection of non-empty sets is non-empty.
moefh · 14h ago
> A human cannot describe said element, by definition.
> The Cartesian product of nonempty sets is nonempty.
I think you want: the Cartesian product of an infinite number of (potentially infinite) non-empty sets is non-empty.
a_cardboard_box · 13h ago
> Note that it's not necessarily simple to pick an element from a set. For instance, how would one pick an element from the set of uncomputable numbers?
In ZF without choice, you can pick an element from any non-empty set, so it actually is simple to pick an element from a set. Choice is only needed when you have an infinite number of sets to pick elements from.
moomin · 14h ago
This seems elegant, but you need that you can take a Cartesian product and turn it into a set of its elements as well. I don’t know if that’s provable without classic AoC. (It might be.)
thaumasiotes · 6h ago
> but you need that you can take a Cartesian product and turn it into a set of its elements as well
Huh? In your model, what is a Cartesian product? How can it have elements without being a set?
throw310822 · 14h ago
Isn't that equivalent (or, ok, similar) to saying that we can decide undecidable mathematical truths?
littlestymaar · 13h ago
As far as I understand there's no such thing “undecidable” in absolute, Gödel incompleteness theorem is about being undecidable under a certain set of axioms.
Sniffnoy · 12h ago
The axiom of choice allows you to make infinitely many arbitrary choices.
You don't need the axiom of choice to make finitely many arbitrary choices. Let's say you have a pile of indistinguishable socks in front of you. You want to pick two of them. Well -- assuming that there are at least two of them to pick -- you can pick one, and then you can pick one from what remains. If something exists, you can pick one of it, that's permitted by the laws of logic; and if you need to do that multiple times, well, obviously you can just do it multiple times. But if you need to do it infinitely many times, well, the laws of logic aren't enough to support that.
You also don't need the axiom of choice if the choices aren't arbitrary, but rather are given by some rule you can specify. There's a famous analogy used by Russell to illustrate this. Suppose you have set in front of you an infinite array of pairs of socks, and you want to pick one sock from each pair. Then you need the axiom of choice to do that. But suppose, instead, it were an infinite array of pairs of shoes. Then you don't need the axiom of choice! Because you can say, I will always pick the left one. That's a rule according to which the choice is made, so you don't need the axiom of choice. You only need the axiom of choice when the choices have some arbitrary element to them, where there isn't a rule you can specify that gets things down to just a single possibility. (Isn't the choice of left over right making an arbitrary choice? In a sense, yeah, but it's only making a single arbitrary choice!)
(The axiom that lets you do this, btw, is the axiom of separation. Or, perhaps in rare instances, the axiom of replacement, but the axiom of replacement is generally irrelevant in normal mathematics.)
So that's what the axiom of choice does. Without it, you can only make finitely many arbitrary choices, or infinitely many specified choices. If you need to make infinitely many choices, but you don't have a rule to do it by, you need axiom of choice.
[Edit: Given the article, I should note that I'm describing the role of the axiom of choice in ordinary mathematics, rather than its role in constructive mathematics. I know little about the latter.]
tel · 6h ago
Often it's easy to construct a family of sets representing something of interest. For example, we like to define integration initially as a finite process of breaking the integrand's domain into pieces, computing their area, and summing.
To compute the contribution of some piece indexed i, we measure the size of its domain, call it the area Ai, and then evaluate the integrand, f, at some point xi within that domain, then the contribution is Ai * f(xi).
Summing all of these across i produces a finite approximation of the integral. Then we take a limit on this process, breaking the domain into larger and larger families of sets with smaller and smaller areas. At the limit, we have the integral.
This process seems intuitive, but it contains an application of the axiom of choice---in the limit, we have an infinite number of subsets of our domain and we still have to pick a representative xi for each one to evaluate the integrand at.
It's quite obvious how to pick an arbitrary representative from each set in a finite family of sets: you just go through one-by-one picking an element.
But this argument breaks down for an infinite family. Going one-by-one will never complete. We need to be able to select these representative xis "all at once". And the Axiom of Choice asserts that this is possible.
(Note: I'm being fast-and-loose, but the nature of the argument is correct. This doesn't prove integration demands AoC or anything like that, just shows how this one sketch of an argument would. Specifically, integration normally avoids AoC because we can constructively specify our choice function - for example, picking the lexicographically smallest point within each axis-aligned rectangular cell. Generalize to something like Monte Carlo integration, however...)
No comments yet
john-h-k · 4h ago
Bertrand Russell coined an analogy: for any (even infinite) collection of pairs of shoes, one can pick out the left shoe from each pair to obtain an appropriate collection (i.e. set) of shoes; this makes it possible to define a choice function directly. For an infinite collection of pairs of socks (assumed to have no distinguishing features such as being a left sock rather than a right sock), there is no obvious way to make a function that forms a set out of selecting one sock from each pair without invoking the axiom of choice.
(From Wikipedia but I’ve always found it good)
krick · 11h ago
Somehow the existing answers don't satisfy me, so here's my attempt. The essence of it is really simple.
The axiom is an obviously true statement: if you have a bag of beans, you can somehow take one bean out of it, without specifying, how do you choose the exact bean. Obvious, right? And that's really it, informally this is the axiom of choice: we are stating that we can somehow always do that, even if there are infinitely many beans and infinitely many bags, and the result of your work may be a collection of infinitely many beans.
Now, what's the "problem"? If you look closer, what I've just said is equivalent to saying we can well-order[0] any set of elements, which must make you uncomfortable: you may be ok with the idea that in principle you can order infinitely many particles of sand (after all, there are just ℕ of them), but how the fuck do you order water (assuming it's like ℝ — there are no molecules and you can divide every drop infinitely many times)?
This is both why we have it — ℝ seems like a useful concept so far; and the source of all notorious "paradoxes" related to it — if you can somehow order water, you may as well be able to reorder details of a sphere in a way to construct 2 spheres of the same size.
If you remember Geometry, there are two ways to prove something:
- By making it (constructing)
- By contradiction (reductio ad absurdum)
During the late 1800s to early 1900s, when math was becoming more formalized, a group of mathematicians had issues with the second method.
From their point of view if you can’t show how to make it, then you’ve not proven that it exists.
Now it turns out that indirect proofs like contradiction requires the law of excluded middle: If something isn’t true, then it must be false (or vice versa).
It turns out that AoC is needed/implied, for the law of excluded middle; hence the objection to AoC; and enables these non-constructive proofs.
Have you ever seen statements such as "for every epsilon there is a delta such that the following ... holds"? The axiom of choice implies that in those cases the delta can be supplied by some function of epsilon. It can't be proven that such a function exists in ordinary ZF (even if you can prove that statement with epsilon and delta).
munificent · 13h ago
The material is way over my head, but, wow, what a beautifully designed page. The layout and typography is delightful.
On the other hand, there's no continuous splitting of the map from the unit interval to the circle that glues together the two endpoints.
So the category of topological spaces does not have the property "every epimorphism splits."
As the article mentions, the axiom of choice says that the category of sets has this property.
So we can think of the various independence results of the 20th century as saying, hey, (assuming ZFC is consistent) 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.
Then whatever, if you want to study something like rings but you don't like the axiom of choice, define a rning to be a snet with two binary operations such that blah blah blah, and you've got a nice category Rning and your various theorems about rnings and maybe they don't all have maximal ideals, even though rings do. You're not arguing about ontology or the nature of truth, you're just picking which category to work in.
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.
- ℕ ∪ {∞}
- 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).
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
> 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.
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."
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?
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 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.
The result is that it is possible for the acceptance of the argument to lead to very different consequences about what we then conclude.
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.)
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).
> 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
There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.
If the latter, what happens if you add to it the (admittedly non-constructive) axiom that the set in question is countable?
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.
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.
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
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.
It isn’t true in NFU though, correct? At least not in the general case. Because Cantor’s argument fails in NFU
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.
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 “CompFunc” 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
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.
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.
> 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:
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 with: 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: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.
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.
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.
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.
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.
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.
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.)
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.
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/
Some of the humans who have thought about it do reject them. Some of the humans who have thought about it don't reject them.
Most humans, including most mathematicians, have never truly thought about it.
I think they reject them only if they misrepresent Hilbert's formalism, because formalism does not assign them any meaning of truth beyond the symbolic. It makes no statement that could be rejected: a mathematical theorem that proves a set "exists" does not necessarily make any claim about its "actual" existence (unlike, say, Platonism). You asked in what sense does such a set exist, and Hilbert would say, great question, which is why I don't claim there necessarily is any such sense.
What those who reject Hilbert's formalism reject is the validity of a system of mathematics where only some but not all propositions are "externally" meaningful, but such a rejection, I think, can only be on aesthetic grounds, because, again, for Hilbert, all "valid" foundations must agree with physical reality when it comes to statements that could be assigned physical meaning. If ZFC led to any result that doesn't agree with physical reality, Hilbert would reject it, too. But it hasn't yet.
If ZFC led to a result that doesn't agree with physical reality, Hilbert would not reject that result. Instead, at worst, he would simply move it from the category of being a real formula, to being an ideal formula. For example, Euclid's geometry doesn't agree with physical reality. Therefore it is an ideal formula, not a real formula. And yet we do not reject this geometry from mathematics.
But the distinction between real and ideal is a question for physics. It is not a question that mathematicians need worry about. The questions that mathematicians need worry about are entirely those which are internal to the formal game.
No. No result, either ideal or real, may contradict reality (it's just that since infinitary statements do not describe reality, they obviously cannot contradict it). You can think about it like this: According to Hilbert, a valid mathematical foundation is any logical theory that is a conservative extension of reality. ZFC, constructive foundations, and ultrafinitist foundations all satisfy that, so they would all be valid foundations according to that principle.
> For example, Euclid's geometry doesn't agree with physical reality.
It may not describe physical reality, but it doesn't contradict it.
> But the distinction between real and ideal is a question for physics. It is not a question that mathematicians need worry about. The questions that mathematicians need worry about are entirely those which are internal to the formal game.
Not only does that disagree with Hilbert's formalism, it also disagrees with constructivism. The question of the philosophy of mathematics is precisely what, if anything, does mathematics describe beyond symbols.
I am also convinced that what you are saying is not what Hilbert actually meant.
But he died before I was born, so I can't ask him. Besides, I don't speak German.
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 ⊢.
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.
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.
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).
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?)
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.
In what sense does an idea exist when it cannot be described by anything on that list?
Regarding “ideas”, to me math is primarily exploration and discovery, rather than invention. That’s one way how it corresponds to the territory analogy.
Maybe these won't be the kind of thing you are looking for, but here are some gems that would be cool to see formalized, some of which I've been meaning to do myself someday:
- There are many parts of the book "A Course in Constructive Algebra" (Mines, Richman, Ruitenburg) worthy of being formalized, but even just the discussion of "omniscience principles" in the first chapter would be cool.
- I absolutely love Sierpinski's book "Cardinal and Ordinal Numbers", and although I'm not sure it would be considered a book of "intuitionistic mathematics", he is careful enough about pointing out where he uses AoC for parts of his book to be suitable for consideration. The results and exercises in VI.5 "Axiom of choice for finite sets" are probably my favorite in the whole book and would be awesome to see formalized.
- Tarski's Theorem about Choice: https://en.wikipedia.org/wiki/Tarski%27s_theorem_about_choic..., particularly from Tarski's original paper (though it is in French).
- I am not sure about a historical article/source for this one, but formalization of some results about Dedekind-finite and Dedekind-infinite sets (https://en.wikipedia.org/wiki/Dedekind-infinite_set) could be really fun. I find these to be very counterintuitive.
And a plug: I have a formalisation of models of constructive set theory in Homotopy Type Theory here: https://git.app.uib.no/hott/hott-set-theory
Is this close to a correct statement of the paper's result? Is all this agreed on today? Have there been any significant refinements?
The modern view on this is homotopy type theory, where types themselves are intrinsically seen as ∞-groupoids (a higher analogue of setoids) and ∃ is interpreted as a propositionally truncated Σ-type (see chapter 3 of the HoTT book). In this setting the axiom of choice says that for any set X, (∀ (x : X). ∥ P x ∥) → ∥ ∀ (x : X). P x ∥ (see section 3.8).
Note that from the perspective of homotopy type theory, Zermelo's axiom of choice is too strong: it is equivalent to global choice (for all types A, ∥ A ∥ → A), which is inconsistent with univalence.
(To explain the joke: they are equivalent, but they strike the intuition very differently.)
It's anti-intuitive:
Disassemble a pea into a finite number of pieces. Then reassemble those pieces to create the sun.
"Finite number of pieces" is a tricky thing. It's a finite number of pieces, sure, but each of those pieces is made of an uncountably infinite number of pieces. Banach-Tarski is a clever way of sweeping an infinite number of dust bunnies under the rug until just the right moment, when it reveals all infinitely many of them in the shape of a pea and claims to have just created them, when in reality, they were actually there all along, hiding under the rug.
For me, Banach-Tarski is just an another version of Hilbert's Hotel, but with uncountable infinities instead of countable ones. Once you accept, in your heart, that infinity is real and is equally deserving of your love and respect as finite natural numbers, then the paradoxicalness of Banach-Tarski melts away.
Such sets, of cause, cannot be constructed or even described as their description will contain infinite number of steps.
> However, the pieces themselves are not "solids" in the traditional sense, but infinite scatterings of points.
But in most cases we want them to reflect the rules of the real world in the sense that statements derived from those axioms reflect our observations. That part (reflect observations) can be separated by many levels of abstractions, etc. I would not try visualizing general statements on Lie algebras or spectral theorems, but those abstractions serve the same goal -- help derive conclusions that apply in the real world. My 2c.
But some math is about providing tools (again, likely via levels of abstractions) for understanding the world and, to me, this is the "real math".
This is a personal view, not an absolute position. I started on the other side of this fence and during my pure math PhD regularly picked fights with our buddies doing physics PhD arguing that mathematics is self-sufficient and does not need any validation from other sciences. But over the next 30 years gradually went to the other side and now think that my original view leads to splintering into gazillion tiny slivers that do not care about anything else; not even about adjacent slivers. Which leads to degeneration. My 2c.
We know what kind of results we want to be true, and then we search for the minimum number of axioms which can deliver that.
This is obvious!, you might say — obviously we can just pick one element from each set and be done with it. But the statement that we can pick an element from each set is the axiom of choice.
Note that it's not necessarily simple to pick an element from a set. For instance, how would one pick an element from the set of uncomputable numbers? A human cannot describe said element, by definition. The axiom of choice says it's possible anyway.
No? I don’t see how this relates to AC at all. AC is about making an infinite number of choices at once – if you’re just making two choices (or, more generally any finite number of choices), as is needed here to prove that this Cartesian product is nonempty, then that’s completely fine without extra axioms. See for example https://mathoverflow.net/q/32538
E.g. in type theory, one term of type `Nonempty(A) → Nonempty(B) → Nonempty(A × B)` (supposing that `Nonempty` is defined as the [bracket type](https://ncatlab.org/nlab/show/bracket+type)) would just be `λ [a] ↦ λ [b] ↦ [(a, b)]`.
https://en.wikipedia.org/wiki/Product_topology#Axiom_of_choi...
>One of many ways to express the axiom of choice is to say that it is equivalent to the statement that the Cartesian product of a collection of non-empty sets is non-empty.
That example doesn't work. Some numbers are describable but not computable, Chaitin's constant being the famous example: https://en.wikipedia.org/wiki/Chaitin%27s_constant
No comments yet
I think you want: the Cartesian product of an infinite number of (potentially infinite) non-empty sets is non-empty.
In ZF without choice, you can pick an element from any non-empty set, so it actually is simple to pick an element from a set. Choice is only needed when you have an infinite number of sets to pick elements from.
Huh? In your model, what is a Cartesian product? How can it have elements without being a set?
You don't need the axiom of choice to make finitely many arbitrary choices. Let's say you have a pile of indistinguishable socks in front of you. You want to pick two of them. Well -- assuming that there are at least two of them to pick -- you can pick one, and then you can pick one from what remains. If something exists, you can pick one of it, that's permitted by the laws of logic; and if you need to do that multiple times, well, obviously you can just do it multiple times. But if you need to do it infinitely many times, well, the laws of logic aren't enough to support that.
You also don't need the axiom of choice if the choices aren't arbitrary, but rather are given by some rule you can specify. There's a famous analogy used by Russell to illustrate this. Suppose you have set in front of you an infinite array of pairs of socks, and you want to pick one sock from each pair. Then you need the axiom of choice to do that. But suppose, instead, it were an infinite array of pairs of shoes. Then you don't need the axiom of choice! Because you can say, I will always pick the left one. That's a rule according to which the choice is made, so you don't need the axiom of choice. You only need the axiom of choice when the choices have some arbitrary element to them, where there isn't a rule you can specify that gets things down to just a single possibility. (Isn't the choice of left over right making an arbitrary choice? In a sense, yeah, but it's only making a single arbitrary choice!)
(The axiom that lets you do this, btw, is the axiom of separation. Or, perhaps in rare instances, the axiom of replacement, but the axiom of replacement is generally irrelevant in normal mathematics.)
So that's what the axiom of choice does. Without it, you can only make finitely many arbitrary choices, or infinitely many specified choices. If you need to make infinitely many choices, but you don't have a rule to do it by, you need axiom of choice.
[Edit: Given the article, I should note that I'm describing the role of the axiom of choice in ordinary mathematics, rather than its role in constructive mathematics. I know little about the latter.]
To compute the contribution of some piece indexed i, we measure the size of its domain, call it the area Ai, and then evaluate the integrand, f, at some point xi within that domain, then the contribution is Ai * f(xi).
Summing all of these across i produces a finite approximation of the integral. Then we take a limit on this process, breaking the domain into larger and larger families of sets with smaller and smaller areas. At the limit, we have the integral.
This process seems intuitive, but it contains an application of the axiom of choice---in the limit, we have an infinite number of subsets of our domain and we still have to pick a representative xi for each one to evaluate the integrand at.
It's quite obvious how to pick an arbitrary representative from each set in a finite family of sets: you just go through one-by-one picking an element.
But this argument breaks down for an infinite family. Going one-by-one will never complete. We need to be able to select these representative xis "all at once". And the Axiom of Choice asserts that this is possible.
(Note: I'm being fast-and-loose, but the nature of the argument is correct. This doesn't prove integration demands AoC or anything like that, just shows how this one sketch of an argument would. Specifically, integration normally avoids AoC because we can constructively specify our choice function - for example, picking the lexicographically smallest point within each axis-aligned rectangular cell. Generalize to something like Monte Carlo integration, however...)
No comments yet
(From Wikipedia but I’ve always found it good)
The axiom is an obviously true statement: if you have a bag of beans, you can somehow take one bean out of it, without specifying, how do you choose the exact bean. Obvious, right? And that's really it, informally this is the axiom of choice: we are stating that we can somehow always do that, even if there are infinitely many beans and infinitely many bags, and the result of your work may be a collection of infinitely many beans.
Now, what's the "problem"? If you look closer, what I've just said is equivalent to saying we can well-order[0] any set of elements, which must make you uncomfortable: you may be ok with the idea that in principle you can order infinitely many particles of sand (after all, there are just ℕ of them), but how the fuck do you order water (assuming it's like ℝ — there are no molecules and you can divide every drop infinitely many times)?
This is both why we have it — ℝ seems like a useful concept so far; and the source of all notorious "paradoxes" related to it — if you can somehow order water, you may as well be able to reorder details of a sphere in a way to construct 2 spheres of the same size.
[0] https://en.wikipedia.org/wiki/Well-ordering_theorem
If you remember Geometry, there are two ways to prove something:
- By making it (constructing)
- By contradiction (reductio ad absurdum)
During the late 1800s to early 1900s, when math was becoming more formalized, a group of mathematicians had issues with the second method.
From their point of view if you can’t show how to make it, then you’ve not proven that it exists.
Now it turns out that indirect proofs like contradiction requires the law of excluded middle: If something isn’t true, then it must be false (or vice versa).
It turns out that AoC is needed/implied, for the law of excluded middle; hence the objection to AoC; and enables these non-constructive proofs.
https://en.m.wikipedia.org/wiki/Law_of_excluded_middle
Another AoC proof: Prove that an irrational number to a irrational power can be rational.
sqrt(2)^sqrt(2) : If rational, then done.
Else (sqrt(2)^sqrt(2))^sqrt(2) = 2.
QED (and non-constructive).
This is provable if everything’s finite, but not if you’re dealing with things with bigger cardinalities like the real numbers.
- Precise statement of the axiom
- Overview of its consequences
- A counterexample (in an alternative universe)
- Consistency of the axiom
- Gödel's sandbox for containing the axiom
https://youtu.be/_cr46G2K5Fo?si=Q6iEm3m-Nyge3FUW
No comments yet