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.
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.
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.
I’m not sure what you mean by “theorems remain the same”. If you take away induction from Peano arithmetic, you get Robinson arithmetic, which has many more models, including (from https://math.stackexchange.com/a/4076545):
- ℕ ∪ {∞}
- Cardinal arithmetic
- ℤ[x]⁺
Obviously, not all theorems that are true for the natural numbers are true for cardinals, so it seems misleading to say that theorems remain the same. I also believe that the addition of induction increases the consistency strength of the theory, so it’s not “just” a matter of expressing the theorems in a different way.
I would agree more for axioms that don’t affect consistency strength, like foundation or choice (over the rest of the ZF axioms).
If I had to write again I might say "same theorems about natural numbers" and capitalize ROUGHLY. It is a conversation, what exactly I am weaseling around (not just nonstandard model theoretic issues), and I take your caveat about consistency strength - with that said would you still call it misleading? Why is it that eg x+y=y+x for x y given takes exponential length proof in Robinson compared to PA? For the reason stated, which is true in a very broad sense.
> If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition
But how can you prove that P(n) for all n without induction? Maybe I misinterpret what you're saying, or I'm naive about something in formal languages, but if we can prove P(n) for all n. then `∀n P(n)` just looks like a trivial transcription of the conclusion into different symbols.
I think the crux of the matter is that we accept inductive arguments as valid, and so we formalize it via the inductive axiom (of Peano arithmetic). i.e., we accept induction as a principle of mathematical reasoning, but we can't derive it from something else so we postualte it when we come around to doing formalizations. Maybe that's what you mean by it coming down to intuition, now that I reread it...
Poincaré has a nice discussion of induction in "On the nature of mathematical reasoning", reprinted in Benacerraf & Putnam Philosophy of Mathematics, where he explicates it as an infinite sequence of modus ponens steps, but irreducible to any more basic logical rule like the principle of (non-)contradiction
>> 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.
> 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."
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.
It doesn't really have to mean anything when we say that the reals are a larger set than the natural numbers - that's just the conclusion of the game that we are playing.
What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?
> What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?
The claim that there are more reals than naturals holds given classical ZF(C) set theory. But there are alternative set theories in which the reals are countable, e.g. NFU+AxCount. These alternative set theories ensure all reals are countable by rendering Cantor’s diagonalisation argument invalid, since their axioms are too weak to validate it. But, they contain all the same reals as the high school mathematics concept of “reals”. So, there are many reals, and that some of them are countable and others are not are indeed “eternal truths” (it is an eternal truth that whatever axioms have the consequences they do), but the everyday (non-expert) concept of reals isn’t any of them in particular - and it is unclear if the dominance of classical notions in mainstream professional mathematics was historically inevitable or a historical accident - maybe, on the other side of the galaxy, there exists some alien civilisation, in which different foundations of mathematics are mainstream, because their mathematics took a different evolutionary course from ours - maybe for them, reals are classically countable, and uncountability is an exotic notion belonging to alternative foundations of mathematics
As I pointed out at https://news.ycombinator.com/item?id=44271589, there are systems that can accept Cantor's argument, without concluding that there are more reals than rational numbers.
As you point out, there are many mathematical systems that contain all of the numbers in the high school mathematics concept of "reals". Since those with a high school understanding of reals do not know which of those systems they would agree with, they should not be asked to accept as true, any results that hold in only some of those systems.
And that is why I don't like mathematicians telling lay audiences that there are more reals than rationals.
"Cantor's diagonalization argument" is best understood as a mere special case of Lawvere's fixed-point theorem. Lawvere's theorem is really the meat of the argument, and it's also the part that is very easy for exotic systems to "accept", since it's close to a purely logical argument. Whether these systems truly accept "Cantor's argument" is perhaps only a matter of perception and intuition, that people may perhaps disagree about.
It does not matter what your best understanding of Cantor's diagonalization argument is. In some mathematical systems it means, "there are more reals than natural numbers", and in others it means, "the reals encode self-reference in a more direct way than the natural numbers do".
The result is that it is possible for the acceptance of the argument to lead to very different consequences about what we then conclude.
> "Cantor's diagonalization argument" is best understood as a mere special case of Lawvere's fixed-point theorem. Lawvere's theorem is really the meat of the argument, and it's also the part that is very easy for exotic systems to "accept", since it's close to a purely logical argument.
Okay, but can you prove Lawvere’s theorem in NFU+AxCount?
And even if you can, since NFU+AxCount proves that the reals are countable, if NFU+AxCount proves Lawvere, then (to echo what btilly says in a sibling comment) NFU+AxCount+Lawvere couldn’t entail the countability of the reals, since that would render NFU+AxCount trivially inconsistent, and we know it is isn’t trivially inconsistent (as with any formal system, consistency is ultimately unprovable, but if a system is taken seriously as an object of mathematical research, then any inconsistency must be highly non-trivial.)
I agree, but I also want to clarify that cantors argument was about subsets of the naturals (N), or more precisely functions from N to Bool (the decidable subsets). This is where the diagonal argument makes sense.
So to conclude that there are more reals than naturals, the classical mathematical argument is:
a) There are more functions N to Bool than naturals.
b) There are as many reals as functions from N to Bool.
Now, we of course agree the mistake is in b) not in a).
> So to conclude that there are more reals than naturals, the classical mathematical argument is:
> a) There are more functions N to Bool than naturals.
> b) There are as many reals as functions from N to Bool.
> Now, we of course agree the mistake is in b) not in a).
Given certain foundations, (a) is false. For example, in the Russian constructivist school (as in Andrey Markov Jr), functions only exist if they are computable, and there are only countably many computable functions from N to Bool. More generally, viewing functions as sets, if you sufficiently restrict the axiom schema of separation/specification, then only countably many sets encoding functions N-to-Bool exist, rendering (a) false
Indeed, what you write is true from an external point of view; just note that within this flavor of constructive mathematics, the set of functions from N to Bool is uncountable again.
There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.
Is it internally uncountable in the strong sense that the system can actually prove the theorem “this set is uncountable”, or only in the weaker sense that it can’t prove the theorem “this set is countable”, but can’t prove its negation either?
If the latter, what happens if you add to it the (admittedly non-constructive) axiom that the set in question is countable?
Suppose that you've written down a function enumerate, that maps all natural numbers to functions that themselves map all natural numbers to booleans. We then can write down the following program.
(defn unenumerated (n) (not ((enumerate n) n)))
This function can be recognized as Cantor diagonalization, written out as a program.
If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.
This argument is, of course, just Cantor's diagonalization argument. From an enumeration, it produces something that can't be in that enumeration.
> If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.
Okay, but if we take the position that only non-halting (for all inputs) programs represent functions over N, if your program “unenumerated” never halts for some N, it doesn’t represent a function, so your argument isn’t a case of “using the enumeration of all functions to produce something which doesn’t belong to the enumeration”
Obviously an enumeration of all computable functions isn’t itself computable. But if we consider Axiom CompFunc “if a function over N is computable then it exists” (so this axiom guarantees the existence of all computable functions, but is silent on whether any non-computable functions exist) and then we consider the additional Axiom CountReals “there exists a function from N to all functions over N”, then are those two axioms mutually inconsistent? I don’t think your argument, as given, directly addresses this question
It's just a straight up liar's paradox. If enumerate is a function that works as advertised, then unenumerated is as well. If enumerate tries to list unenumerated, then enumerate can't work as advertised.
For the argument that I gave to work, you need what you might call Axiom ComposeFunc, you may always compose a new function by taking an existing function and doing something that is known to be valid with it. Obviously this axiom is true about the computable universe. But, more than that, it is also true about any generalization of "function" that behaves like most would expect a function to have.
Now it is true that your Axiom CompFunc and Axiom CountReals do not necessarily contradict each other. But CompFunc, ComposeFunc and CountReals do contradict each other, and the contradiction can be built by following Cantor's diagonalization argument.
If I understand what I just Googled correctly (definitely not guaranteed), the reason why Cantor's argument can fail in NFU is that NFU does not necessarily allow you to build a function that returns things in X, out of a function that returns functions returning things in X.
So it has non-computable functions, but also has a type system that tries to avoid allowing self-reference. And that type system gets in the way of Cantor's argument.
I clearly hadn't thought of this possibility. It is a constraint of a kind that doesn't show up in the computable universe.
And so, going back, if the the Russian constructivist school does indeed center on computability, then my first answer to you was correct.
Right, I think we are in agreement - a pure Russian constructivist approach which only permits computable functions cannot prove the reals are countable. However, I still am sceptical it can prove they are uncountable-if you limit yourself to computable constructions, you can’t actually computably construct a Cantor diagonal, so his argument fails just like it does in NFU.
The (un)countability of the reals is known to be independent of NFU-it is consistent both with the reals being countable and them being uncountable. There are two different axioms which it is standard to add to NFU to decide this-AxCount≤ which implies the reals are countable and AxCount≥ which implies the reals are uncountable.
I guess I was suggesting that in the same way, an additional axiom could be added to computable set theory which renders the reals countable or uncountable. If an additional axiom asserting the countability of the reals involves the existence of a function from the naturals to functions over the naturals, that would obviously be introducing an uncomputable function-but for that to produce an inconsistency, it would need to enable Cantor’s argument-and, given your “ComposeFunc” in the computable universe is already restricted to only operating over computable functions, it is reasonable to limit its application to computable functions in an extension, which would mean the addition of this uncomputable function would still not permit Cantor’s argument
There is nothing uncomputable with the cantor diagonalisation. The Russians gladly accept it, I assure you. Here is a Haskell implementation:
diag :: (nat -> (nat -> Bool)) -> (nat -> Bool)
diag f n = not (f n n)
The following argument is also constructive. Just like in classical mathematics, crustructive mathematics proves the negation of A by assuming A and deriving a contradiction. (But you cannot prove A by assuming it’s negation and deriving a contraction):
Assume a surjectiom f :: nat -> Bool. Then there is x such that f x = diag f. Since these two functions are equal, they take equal values when we evaluate them in any point. In particular f x x = diag f x, but since diag f x = not (f x x), by definition, we have that f x x = not (f x x). This is a contradiction since not does not have fixed points.
( I made nat a type variable here since this works for any type / set )
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.
How is it different from using ZF as a meta-theory to study ZF(C)? Is there anything special about category theory vis-à-vis ZF as a meta-theory? You're not arguing about ontology or the nature of truth, because you've picked category theory as your ontology just like you could pick ZF or ZFC.
Category theory gives a structural framework for discussing these things. The various categories live side by side and can be related with functors. This allows a broader view and makes it easier perhaps, to understand that there isn’t a right answer to “what is true” about sets in the absolute.
For sure there would have to be a meta theory of some sort. But, I think that many classical mathematicians would be happy with that meta theory to be weaker, rather than stronger. I don't think there is a need for that theory to have AC. After all, thanks to its independence of from the other axioms, AC does not add logical strength to a classical theory.
(For die-hard constructivists, such as myself, the story is of course different. But that story is for a another time. I am presenting the classical view here.)
Yes, but the parent comment is trying to say "imagine the world would only be made up of topological spaces and continuous maps". Then the retraction principle would not hold.
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.
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.
> 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
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.
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.
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.
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.
> 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.
> 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.
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.)
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.
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.
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
> 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.
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.
> 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.
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.
> I have absolutely no idea how physical reality can contradict a statement about a formal symbol game.
Of course it can! For example, if some logic theory contains the theorem that a particular realisable polynomial-time algorithm that can solve an EXPTIME-hard problem, that would contradict physical reality.
I should clarify that when I talk about "physical reality" that's shorthand for things that are, at least in principle, verifiable using physical means.
> 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.
Ok, but if you're not sure what a certain philosophical position is, surely you cannot find fault with it. But I was able to locate my Heijenoort, so we can try, assuming you trust Heijenoort's translation.
So here's just a tidbit from Hilbert's 1925 "On The Infinite" (Heijenoort p.367):
And the net result is, certainly, that we do not find anywhere in reality a homogeneous continuum that permits of continued division and hence would realize the infinite in the small. The infinite divisibility of a continuum is an operation that is present only in ourthoughts; it is merely an idea, which is refuted by our observations of nature and by the experience gained in physics and chemistry.
And here are parts of Hilbert, 1927, "The foundations of mathematics" (Heijenoort p.464):
All the propositions that constitute mathematics are converted into formulas, so
that mathematics proper becomes an inventory of formulas.
...even elementary mathematics contains, first, formulas to which correspond contentual communications of finitary propositions (mainly numerical equations or inequalities, or more complex communications composed of these) and which we may
call the real propositions of the theory, and, second, formulas that -just like the numerals of contentual number theory - in themselves mean nothing but are merely things that are governed by our rules and must be regarded as the ideal objects of the theory.
These considerations show that, to arrive at the conception of formulas as ideal propositions, we need only pursue in a natural and consistent way the line of development that mathematical practice has already followed till now.
... Now the fundamental difficulty that we face here can be avoided by the use of ideal propositions. For, if to the real propositions we adjoin the ideal ones, we obtain a system of propositions in which all the simple rules of Aristotelian logic hold and all the usual methods of mathematical inference are valid.
... To be sure, one condition, a single but indispensable one, is always attached to the use of the method of ideal elements, and that is the proof of consistency; for, extension by the addition of ideal elements is legitimate only if no contradiction is thereby brought about in the old, narrower domain, that is, if the relations that result for the old objects whenever the ideal objects are eliminated are valid in the old domain.
... To make it a universal requirement that each individual formula then be interpretable by itself is by no means reasonable; on the contrary, a theory by its very nature is such that we do not need to fall back upon intuition or meaning in the midst of some argument. What the physicist demands precisely of a theory is that particular propositions be derived from laws of nature or hypotheses solely by inferences, hence on the basis of a pure formula game, without extraneous considerations being adduced. Only certain combinations and consequences of the physical laws can be checked by experiment just as in my proof theory only the real propositions are directly capable of verification.
The value of pure existence proofs consists precisely in that the individual construction is eliminated by them and that many different constructions are subsumed under one fundamental idea, so that only what is essential to the proof stands out clearly; brevity and economy of thought are the raison d'être of existence proofs.
In other words, "ideal" propositions may mean nothing in and of themselves but they are valid as long as they are a conservative extension of the "real" propositions (the narrower domain), which are necessarily meaningful as they are "directly capable of verification".
> Of course it can! For example, if some logic theory contains the theorem that a particular realisable polynomial-time algorithm that can solve an EXPTIME-hard problem, that would contradict physical reality.
It would only contradict physical reality if a machine to calculate that algorithm failed to solve the EXPTIME-hard problem as promised. And if it failed to do that, I am confident that the problem is a mistake in the logic theory proof.
As for your long quote from Hilbert, I understand it very differently from you. He is saying that our interest in ideal mathematics starts with real mathematics. But ideal mathematics is something to engage with on its own terms, whether or not it corresponds with anything real.
Basically he's just saying, "Math is a formal game. People got interested in this game because part of the game corresponds to things we experience in reality." But that doesn't mean that the game itself depends in any way upon physical reality - it exists in its own terms.
> And if it failed to do that, I am confident that the problem is a mistake in the logic theory proof.
You can axiomatically add oracles without introducing logical inconsistencies. It is commonly done in complexity theory. The "mistake" is in interpreting such results as directly corresponding to the real world (same as interpreting 2 + 1 = 0 in modular arithmetic as if it were saying something about natural numbers). That is Hilbert's point: we need to be clear about how we map certain mathematical statements to the real world, and "to make it a universal requirement that each individual formula then be interpretable by itself is by no means reasonable", i.e. even when we're clear about such a mapping, it is not a requirement that every forumla had such a mapping. Or, perhaps more clear, Hilbert's point is that if in a logical theory not every formula can be assigned a "real meaning", that does not invalidate assigning real meaning to some formulas.
> Basically he's just saying, "Math is a formal game. People got interested in this game because part of the game corresponds to things we experience in reality." But that doesn't mean that the game itself depends in any way upon physical reality - it exists in its own terms.
He is very explicit that he is not saying that about the "real" propositions. He calls them "contentual", as in carrying content beyond the symbols. From the same talk:
If we now begin to construct mathematics, we shall first set our sights upon elementary number theory; we recognize that we can obtain and prove its truths through contentual intuitive considerations. The formulas that we encounter when we take this approach are used only to impart information.
He is very clear that the justification for the use of formulas that are "just a symbols game" is that they are consistent with formulas that are contentual and are not just a symbols game. That is the debate between Hilbert and Brouwer, or formalism and intuitionism: whether or not all formulas must have an intuitive meaning ("content"). In formalism, not all of them must.
It is precisely because Hilbert's justification was based on consistency, as without it, "real" propositions could be wrong, that the incompleteness results made that justification unprovable.
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.
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.
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).
> 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 ⊢.
Gödel's incompleteness theorem tells you why it is a good idea to separate semantics (notion of truth) from syntax (reasoning). Because some things are true, although you cannot prove that they are.
Some people now put forward from this the idea that for the natural numbers we know, it is NOT either true or false if for example the twin prime conjecture holds. That is nonsense. It is just that our methods of proof are strictly weaker than our notion of truth is.
That this is so is not even surprising! It is a fact of life that what is true is not necessarily what you can prove to be true. Innocent people imprisoned are an example of that. Guilty people going free another. What is maybe surprising is that what is true in what we perceive as the "real world" is also true in mathematics, which we imagine to be an "ideal realm". But mathematics is ALSO part of the "real world"; if you understand this, it is not so surprising. Yes, I am a platonist, and I think that everybody who isn't is just plain wrong and confused.
Intensional functions are just a special case of extensional functions. Where extensional functions are defined on mathematical objects, intensional functions are extensional functions defined on representations of mathematical objects (which are also mathematical objects, by the way), but pretend to be acting on the mathematical objects themselves, not their representations. That is really all there is to it, it is not a deep philosophical mystery. To do so can of course be very useful!
> there is a single countable list that includes all things that might possibly have any mathematical existence at all.
Help me understand that. Isn't the Cantor diagonialization argument a proof that such a list cannot exist because, supposing it did exist, it could be used to construct an object not on the list? Are you proposing that your list somehow defeats Cantor here?
(Of course, we're using the word "list" loosely here. What we mean is a total function with domain Nat, right?)
> all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist.
The universe (in the cosmological sense) can be written down as a single countable list, and anything different would be impossible? Or are you saying that it does not truly exist? I’m not sure how that makes sense.
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?
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.
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?
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.
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?
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
There arguably has been a failure of communication between type theorists and "traditional" mathematicians, but Buzzard unfortunately has a bit of a history of vocally spreading less-than-accurate information about type theory. I'd suggest not focusing too much on this one person's opinions and engaging with the subject for yourself if it interests you.
It's also worth keeping in mind that mathematicians traditionally haven't cared too much about foundations, and are not necessarily the best people to ask about them; see Hilbert, Bourbaki and the scorning of logic¹. Among people who are interested in foundations (logicians, category theorists, computer scientists, philosophers, ...), there is a pretty clear consensus that HoTT is a major step forward; but of course it's not the kind of "step forward" with immediate, observable results. As David Madore puts it, you wouldn't cut the roots of an apple tree just because no apples grow there.
> but of course it's not the kind of "step forward" with immediate, observable results.
Nice, it looks like you agree with Kevin Buzzard's claim about HoTT in the presentation I linked above. While mathematicians as a whole have historically not cared all that much about the practicality of formal foundations, it's worth noting that Kevin Buzzard has quite some expertise in dealing with the Grothendieck-style fuzzy, informal reasoning about equality that happens to be a key motivation behind HoTT itself and the univalence approach. What he seems to claim on the topic is that HoTT makes it a tiny bit easier to phrase a formal treatment of these issues, but you still have to do all the really hard work of proving that everything "respects" the equalities you claim it respects. The fact that you can then "transport" mathematical objects, proofs etc. along equalities is nifty but is also the kind of thing that would be glossed over to begin with in any informal treatment, so there's no real gain wrt. that.
Do you have a reference for that, such as a podcast link? His paper on Grothendieck's use of equality is implicitly rather critical of HoTT proponents' claims anyway (which is why I linked that too), but I'm curious to know if he has publicly said anything more specific than that.
Thanks for the reference! That take of his sounds a bit confused in-context (univalence and constructivism are not directly related, you can work non-constructively and still use the overall featureset of HoTT/univalence) but then his remark about how he's just working on non-constructive stuff that we don't even know how to phrase constructively is just fair.
Relatedly, the kind of philosophical constructivism that would make claims like "non-constructive mathematics is just wrong and useless" has been a bit problematic in many ways, he's not totally off-base about this.
I disliked his skepticism about proofs-as-programs the most, but that's because I think "a direct proof is a program" is very much a worthwhile statement. Of course some mathematicians will opt not to care about that.
> 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.
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.
> 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)]`.
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.
>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.
> 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.
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.)
Well, you’d need some model of index, for one. And I’m not sure how you’d construct that with uncountably many elements. Even ignoring that, a set containing n elements is different from a set containing n sets of one element each.
Not saying your formulation is wrong, just that there’s a fair amount of non-obvious work to get to the classic formulation.
> Even ignoring that, a set containing n elements is different from a set containing n sets of one element each.
Different in what way? A set containing n sets of one element each is a set containing n elements.
In ZF, everything that's an element of a set is itself a set, so unless what's bothering you is the idea that "a set containing n elements" might contain the empty set, or a set with two elements, I'm not seeing it.
> you’d need some model of index, for one. And I’m not sure how you’d construct that with uncountably many elements
Why would the number of elements matter? Set elements aren't indexed. What are you using your model of index for?
I really feel I should repeat the question I asked you to begin with: You say you need to convert a Cartesian product into a set containing "its elements". In your mind, what is a Cartesian product, before that conversion takes place?
Okay, let’s simplify. Do we agree that the Cartesian product (a,b,c,a) is represented in ZFC as
{{1 a} {2 b} {3 c} {4 d}} and that that is different from {a b c a}?
Well, it's true that tuples aren't defined by the ZF axioms. They do have a conventional definition, which you appear not to know.†
Natural numbers also aren't defined by the ZF axioms; why do you think that the definition of a tuple should involve them? You're likely to have a hard time finding a textbook that agrees.
I'm getting an overwhelming sense here that you don't know the meaning of the things you say. If you don't know what a Cartesian product is, why do you think it makes sense to talk about what you can and can't do with it?
Why do you think it makes sense to write {a b c a}, which has no meaning?
† For reference: by the standard convention, the tuple (a, b, c, a) is represented as the set {{{a, {a, b}}, {{a, {a, b}}, c}}, {{{a, {a, b}}, {{a, {a, b}}, c}, a}}. You might notice that no numbers appear anywhere. You might also notice that regardless of representation - and you're free to use other representations - it will never be a Cartesian product, because "tuple" and "Cartesian product" refer to different things.
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.
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.]
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.
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.
The single most best definition I know is what is on the wiki[0]:
> A choice function (also called selector or selection) is a function f, defined on a collection X of nonempty sets, such that for every set A in X, f(A) is an element of A. With this concept, the axiom can be stated:
> Axiom—For any set X of nonempty sets, there exists a choice function f that is defined on X and maps each set of X to an element of that set.
I like this definition because IMO it is simple, close to the name of the axiom, and you might want to use it in this form, that is, having a set of sets, and taking a choice function on them.
To understand its importance and the controversies around it, you'll need some examples and counterexamples how truthness and provability and knowability (regarding structures, numbers, metamathematics) interact; also what are the views of the majority of working mathematicians and people in other fields using mathematics.
Tangential, but a choice function is one of the ur-examples of Dependent Type Theory (DTT). In standard ZFC the choice function on X would have the type signature
f: X -> UX (union X).
And you know the additional information that (∀A:X) (f(A) ∈ A), which is not encoded in the type signature, just an additional fact that you know, and have to keep track of it. In DTT the codomain can be the function of the picked element of the domain. In this case, the DTT type signature of f would be
f: (A:X) -> A.
So in this case the signature of the function carries strictly more information than in the case of normal, static function type signatures in ZFC. And the axiom of choice simply states that the type (A:X) -> A is non-empty if every A are non-empty.
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...)
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).
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.
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.
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.
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.
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.
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.
I’m not sure what you mean by “theorems remain the same”. If you take away induction from Peano arithmetic, you get Robinson arithmetic, which has many more models, including (from https://math.stackexchange.com/a/4076545):
- ℕ ∪ {∞}
- Cardinal arithmetic
- ℤ[x]⁺
Obviously, not all theorems that are true for the natural numbers are true for cardinals, so it seems misleading to say that theorems remain the same. I also believe that the addition of induction increases the consistency strength of the theory, so it’s not “just” a matter of expressing the theorems in a different way.
I would agree more for axioms that don’t affect consistency strength, like foundation or choice (over the rest of the ZF axioms).
If I had to write again I might say "same theorems about natural numbers" and capitalize ROUGHLY. It is a conversation, what exactly I am weaseling around (not just nonstandard model theoretic issues), and I take your caveat about consistency strength - with that said would you still call it misleading? Why is it that eg x+y=y+x for x y given takes exponential length proof in Robinson compared to PA? For the reason stated, which is true in a very broad sense.
> If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition
But how can you prove that P(n) for all n without induction? Maybe I misinterpret what you're saying, or I'm naive about something in formal languages, but if we can prove P(n) for all n. then `∀n P(n)` just looks like a trivial transcription of the conclusion into different symbols.
I think the crux of the matter is that we accept inductive arguments as valid, and so we formalize it via the inductive axiom (of Peano arithmetic). i.e., we accept induction as a principle of mathematical reasoning, but we can't derive it from something else so we postualte it when we come around to doing formalizations. Maybe that's what you mean by it coming down to intuition, now that I reread it...
Poincaré has a nice discussion of induction in "On the nature of mathematical reasoning", reprinted in Benacerraf & Putnam Philosophy of Mathematics, where he explicates it as an infinite sequence of modus ponens steps, but irreducible to any more basic logical rule like the principle of (non-)contradiction
>> 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.
> 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."
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.
Good point. I would argue, however, that having nicer proofs is a "useful" result of the game.
Spoken like a true formalist.
It doesn't really have to mean anything when we say that the reals are a larger set than the natural numbers - that's just the conclusion of the game that we are playing.
What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?
> What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?
The claim that there are more reals than naturals holds given classical ZF(C) set theory. But there are alternative set theories in which the reals are countable, e.g. NFU+AxCount. These alternative set theories ensure all reals are countable by rendering Cantor’s diagonalisation argument invalid, since their axioms are too weak to validate it. But, they contain all the same reals as the high school mathematics concept of “reals”. So, there are many reals, and that some of them are countable and others are not are indeed “eternal truths” (it is an eternal truth that whatever axioms have the consequences they do), but the everyday (non-expert) concept of reals isn’t any of them in particular - and it is unclear if the dominance of classical notions in mainstream professional mathematics was historically inevitable or a historical accident - maybe, on the other side of the galaxy, there exists some alien civilisation, in which different foundations of mathematics are mainstream, because their mathematics took a different evolutionary course from ours - maybe for them, reals are classically countable, and uncountability is an exotic notion belonging to alternative foundations of mathematics
As I pointed out at https://news.ycombinator.com/item?id=44271589, there are systems that can accept Cantor's argument, without concluding that there are more reals than rational numbers.
As you point out, there are many mathematical systems that contain all of the numbers in the high school mathematics concept of "reals". Since those with a high school understanding of reals do not know which of those systems they would agree with, they should not be asked to accept as true, any results that hold in only some of those systems.
And that is why I don't like mathematicians telling lay audiences that there are more reals than rationals.
"Cantor's diagonalization argument" is best understood as a mere special case of Lawvere's fixed-point theorem. Lawvere's theorem is really the meat of the argument, and it's also the part that is very easy for exotic systems to "accept", since it's close to a purely logical argument. Whether these systems truly accept "Cantor's argument" is perhaps only a matter of perception and intuition, that people may perhaps disagree about.
It does not matter what your best understanding of Cantor's diagonalization argument is. In some mathematical systems it means, "there are more reals than natural numbers", and in others it means, "the reals encode self-reference in a more direct way than the natural numbers do".
The result is that it is possible for the acceptance of the argument to lead to very different consequences about what we then conclude.
> "Cantor's diagonalization argument" is best understood as a mere special case of Lawvere's fixed-point theorem. Lawvere's theorem is really the meat of the argument, and it's also the part that is very easy for exotic systems to "accept", since it's close to a purely logical argument.
Okay, but can you prove Lawvere’s theorem in NFU+AxCount?
And even if you can, since NFU+AxCount proves that the reals are countable, if NFU+AxCount proves Lawvere, then (to echo what btilly says in a sibling comment) NFU+AxCount+Lawvere couldn’t entail the countability of the reals, since that would render NFU+AxCount trivially inconsistent, and we know it is isn’t trivially inconsistent (as with any formal system, consistency is ultimately unprovable, but if a system is taken seriously as an object of mathematical research, then any inconsistency must be highly non-trivial.)
I agree, but I also want to clarify that cantors argument was about subsets of the naturals (N), or more precisely functions from N to Bool (the decidable subsets). This is where the diagonal argument makes sense.
So to conclude that there are more reals than naturals, the classical mathematical argument is:
a) There are more functions N to Bool than naturals.
b) There are as many reals as functions from N to Bool.
Now, we of course agree the mistake is in b) not in a).
> So to conclude that there are more reals than naturals, the classical mathematical argument is:
> a) There are more functions N to Bool than naturals.
> b) There are as many reals as functions from N to Bool.
> Now, we of course agree the mistake is in b) not in a).
Given certain foundations, (a) is false. For example, in the Russian constructivist school (as in Andrey Markov Jr), functions only exist if they are computable, and there are only countably many computable functions from N to Bool. More generally, viewing functions as sets, if you sufficiently restrict the axiom schema of separation/specification, then only countably many sets encoding functions N-to-Bool exist, rendering (a) false
Indeed, what you write is true from an external point of view; just note that within this flavor of constructive mathematics, the set of functions from N to Bool is uncountable again.
There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.
Is it internally uncountable in the strong sense that the system can actually prove the theorem “this set is uncountable”, or only in the weaker sense that it can’t prove the theorem “this set is countable”, but can’t prove its negation either?
If the latter, what happens if you add to it the (admittedly non-constructive) axiom that the set in question is countable?
It should be true in the stronger sense.
Suppose that you've written down a function enumerate, that maps all natural numbers to functions that themselves map all natural numbers to booleans. We then can write down the following program.
This function can be recognized as Cantor diagonalization, written out as a program.If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.
This argument is, of course, just Cantor's diagonalization argument. From an enumeration, it produces something that can't be in that enumeration.
> If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.
Okay, but if we take the position that only non-halting (for all inputs) programs represent functions over N, if your program “unenumerated” never halts for some N, it doesn’t represent a function, so your argument isn’t a case of “using the enumeration of all functions to produce something which doesn’t belong to the enumeration”
Obviously an enumeration of all computable functions isn’t itself computable. But if we consider Axiom CompFunc “if a function over N is computable then it exists” (so this axiom guarantees the existence of all computable functions, but is silent on whether any non-computable functions exist) and then we consider the additional Axiom CountReals “there exists a function from N to all functions over N”, then are those two axioms mutually inconsistent? I don’t think your argument, as given, directly addresses this question
It's just a straight up liar's paradox. If enumerate is a function that works as advertised, then unenumerated is as well. If enumerate tries to list unenumerated, then enumerate can't work as advertised.
For the argument that I gave to work, you need what you might call Axiom ComposeFunc, you may always compose a new function by taking an existing function and doing something that is known to be valid with it. Obviously this axiom is true about the computable universe. But, more than that, it is also true about any generalization of "function" that behaves like most would expect a function to have.
Now it is true that your Axiom CompFunc and Axiom CountReals do not necessarily contradict each other. But CompFunc, ComposeFunc and CountReals do contradict each other, and the contradiction can be built by following Cantor's diagonalization argument.
> But, more than that, it is also true about any generalization of "function" that behaves like most would expect a function to have.
It isn’t true in NFU though, correct? At least not in the general case. Because Cantor’s argument fails in NFU
If I understand what I just Googled correctly (definitely not guaranteed), the reason why Cantor's argument can fail in NFU is that NFU does not necessarily allow you to build a function that returns things in X, out of a function that returns functions returning things in X.
So it has non-computable functions, but also has a type system that tries to avoid allowing self-reference. And that type system gets in the way of Cantor's argument.
I clearly hadn't thought of this possibility. It is a constraint of a kind that doesn't show up in the computable universe.
And so, going back, if the the Russian constructivist school does indeed center on computability, then my first answer to you was correct.
Right, I think we are in agreement - a pure Russian constructivist approach which only permits computable functions cannot prove the reals are countable. However, I still am sceptical it can prove they are uncountable-if you limit yourself to computable constructions, you can’t actually computably construct a Cantor diagonal, so his argument fails just like it does in NFU.
The (un)countability of the reals is known to be independent of NFU-it is consistent both with the reals being countable and them being uncountable. There are two different axioms which it is standard to add to NFU to decide this-AxCount≤ which implies the reals are countable and AxCount≥ which implies the reals are uncountable.
I guess I was suggesting that in the same way, an additional axiom could be added to computable set theory which renders the reals countable or uncountable. If an additional axiom asserting the countability of the reals involves the existence of a function from the naturals to functions over the naturals, that would obviously be introducing an uncomputable function-but for that to produce an inconsistency, it would need to enable Cantor’s argument-and, given your “ComposeFunc” in the computable universe is already restricted to only operating over computable functions, it is reasonable to limit its application to computable functions in an extension, which would mean the addition of this uncomputable function would still not permit Cantor’s argument
There is nothing uncomputable with the cantor diagonalisation. The Russians gladly accept it, I assure you. Here is a Haskell implementation:
diag :: (nat -> (nat -> Bool)) -> (nat -> Bool)
diag f n = not (f n n)
The following argument is also constructive. Just like in classical mathematics, crustructive mathematics proves the negation of A by assuming A and deriving a contradiction. (But you cannot prove A by assuming it’s negation and deriving a contraction):
Assume a surjectiom f :: nat -> Bool. Then there is x such that f x = diag f. Since these two functions are equal, they take equal values when we evaluate them in any point. In particular f x x = diag f x, but since diag f x = not (f x x), by definition, we have that f x x = not (f x x). This is a contradiction since not does not have fixed points.
( I made nat a type variable here since this works for any type / set )
Bringing in computability from an external point of view is a mistake here. Markov had no issue with a. He would only disagree with b.
> Spoken like a true formalist.
Doesn't seem to be a bad thing. There are some famous cranks who reject the concept of infinity, since I suppose they have problems wrapping their head around it.
> What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?
People misunderstand mathematics all the time. It's ok, it's part of the journey.
How is it different from using ZF as a meta-theory to study ZF(C)? Is there anything special about category theory vis-à-vis ZF as a meta-theory? You're not arguing about ontology or the nature of truth, because you've picked category theory as your ontology just like you could pick ZF or ZFC.
Category theory gives a structural framework for discussing these things. The various categories live side by side and can be related with functors. This allows a broader view and makes it easier perhaps, to understand that there isn’t a right answer to “what is true” about sets in the absolute.
But then you would think there is a right answer to “what is true” about categories, and you would face AC again.
For sure there would have to be a meta theory of some sort. But, I think that many classical mathematicians would be happy with that meta theory to be weaker, rather than stronger. I don't think there is a need for that theory to have AC. After all, thanks to its independence of from the other axioms, AC does not add logical strength to a classical theory.
(For die-hard constructivists, such as myself, the story is of course different. But that story is for a another time. I am presenting the classical view here.)
Doesn't "continuous" make all the difference here? AC doesn't contain a comparable limitation, so the analogy doesn't work that week.
Yes, but the parent comment is trying to say "imagine the world would only be made up of topological spaces and continuous maps". Then the retraction principle would not hold.
Careful here, you might wake up the diabol (of pure algebra)
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.
I wish that I had specific suggestions.
My overall wish that more people understood why, in intuitionist mathematics, uncountable means "self-referential" and not "more". No infinite set can have "more" elements than any other, because all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist.
(By internet coincidence, I recently wrote https://math.stackexchange.com/questions/5074503/can-pa-prov... which ends with the beginning of the construction of that list, starting with the Peano axioms. https://news.ycombinator.com/item?id=44269822 is about that answer.)
Of course Formalists simply write down some axioms, start constructing proofs, and don't worry about what it really means. In what sense do uncountable hordes of real numbers that can never be specified in any way, truly exist? It doesn't matter. These are the axioms that we chose, and that is the statement that we came up with.
I have no idea of whether there is a way to formalize or prove the following idea. If there is, it would be good to mechanize it.
All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth.
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:
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: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.
Relevant to this is Skolem’s paradox (https://en.wikipedia.org/wiki/Skolem%27s_paradox), which states that any uncountable set can be modelled by a countable set.
In that light, the statement that the reals have greater cardinality than the naturals can be thought of as a statement that _our model of set theory_ happens to contain no injections from the reals to the naturals. Not that they can’t exist in a Platonic sense, or even just in the metatheory.
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.
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.
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.
> 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.
> 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.
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.)
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.
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.
I thought it was generally understood that Hilbert didn’t literally believe that. Do you seriously believe that he believed it?
What I said about Hilbert's belief was a quote by him. So of course I believe it.
His full views were more complicated, and are already discussed elsewhere in this discussion.
My statement about Gödel is not an exact quote, but fits what I've heard from every source on the topic. He was a very deeply religious genius.
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 mean people who have thought about it.
[1]: https://plato.stanford.edu/entries/hilbert-program/
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.
> 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.
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.
> 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.
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.
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.
> I have absolutely no idea how physical reality can contradict a statement about a formal symbol game.
Of course it can! For example, if some logic theory contains the theorem that a particular realisable polynomial-time algorithm that can solve an EXPTIME-hard problem, that would contradict physical reality.
I should clarify that when I talk about "physical reality" that's shorthand for things that are, at least in principle, verifiable using physical means.
> 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.
Ok, but if you're not sure what a certain philosophical position is, surely you cannot find fault with it. But I was able to locate my Heijenoort, so we can try, assuming you trust Heijenoort's translation.
So here's just a tidbit from Hilbert's 1925 "On The Infinite" (Heijenoort p.367):
And the net result is, certainly, that we do not find anywhere in reality a homogeneous continuum that permits of continued division and hence would realize the infinite in the small. The infinite divisibility of a continuum is an operation that is present only in ourthoughts; it is merely an idea, which is refuted by our observations of nature and by the experience gained in physics and chemistry.
And here are parts of Hilbert, 1927, "The foundations of mathematics" (Heijenoort p.464):
All the propositions that constitute mathematics are converted into formulas, so that mathematics proper becomes an inventory of formulas.
...even elementary mathematics contains, first, formulas to which correspond contentual communications of finitary propositions (mainly numerical equations or inequalities, or more complex communications composed of these) and which we may call the real propositions of the theory, and, second, formulas that -just like the numerals of contentual number theory - in themselves mean nothing but are merely things that are governed by our rules and must be regarded as the ideal objects of the theory.
These considerations show that, to arrive at the conception of formulas as ideal propositions, we need only pursue in a natural and consistent way the line of development that mathematical practice has already followed till now.
... Now the fundamental difficulty that we face here can be avoided by the use of ideal propositions. For, if to the real propositions we adjoin the ideal ones, we obtain a system of propositions in which all the simple rules of Aristotelian logic hold and all the usual methods of mathematical inference are valid.
... To be sure, one condition, a single but indispensable one, is always attached to the use of the method of ideal elements, and that is the proof of consistency; for, extension by the addition of ideal elements is legitimate only if no contradiction is thereby brought about in the old, narrower domain, that is, if the relations that result for the old objects whenever the ideal objects are eliminated are valid in the old domain.
... To make it a universal requirement that each individual formula then be interpretable by itself is by no means reasonable; on the contrary, a theory by its very nature is such that we do not need to fall back upon intuition or meaning in the midst of some argument. What the physicist demands precisely of a theory is that particular propositions be derived from laws of nature or hypotheses solely by inferences, hence on the basis of a pure formula game, without extraneous considerations being adduced. Only certain combinations and consequences of the physical laws can be checked by experiment just as in my proof theory only the real propositions are directly capable of verification.
The value of pure existence proofs consists precisely in that the individual construction is eliminated by them and that many different constructions are subsumed under one fundamental idea, so that only what is essential to the proof stands out clearly; brevity and economy of thought are the raison d'être of existence proofs.
In other words, "ideal" propositions may mean nothing in and of themselves but they are valid as long as they are a conservative extension of the "real" propositions (the narrower domain), which are necessarily meaningful as they are "directly capable of verification".
> Of course it can! For example, if some logic theory contains the theorem that a particular realisable polynomial-time algorithm that can solve an EXPTIME-hard problem, that would contradict physical reality.
It would only contradict physical reality if a machine to calculate that algorithm failed to solve the EXPTIME-hard problem as promised. And if it failed to do that, I am confident that the problem is a mistake in the logic theory proof.
As for your long quote from Hilbert, I understand it very differently from you. He is saying that our interest in ideal mathematics starts with real mathematics. But ideal mathematics is something to engage with on its own terms, whether or not it corresponds with anything real.
Basically he's just saying, "Math is a formal game. People got interested in this game because part of the game corresponds to things we experience in reality." But that doesn't mean that the game itself depends in any way upon physical reality - it exists in its own terms.
> And if it failed to do that, I am confident that the problem is a mistake in the logic theory proof.
You can axiomatically add oracles without introducing logical inconsistencies. It is commonly done in complexity theory. The "mistake" is in interpreting such results as directly corresponding to the real world (same as interpreting 2 + 1 = 0 in modular arithmetic as if it were saying something about natural numbers). That is Hilbert's point: we need to be clear about how we map certain mathematical statements to the real world, and "to make it a universal requirement that each individual formula then be interpretable by itself is by no means reasonable", i.e. even when we're clear about such a mapping, it is not a requirement that every forumla had such a mapping. Or, perhaps more clear, Hilbert's point is that if in a logical theory not every formula can be assigned a "real meaning", that does not invalidate assigning real meaning to some formulas.
> Basically he's just saying, "Math is a formal game. People got interested in this game because part of the game corresponds to things we experience in reality." But that doesn't mean that the game itself depends in any way upon physical reality - it exists in its own terms.
He is very explicit that he is not saying that about the "real" propositions. He calls them "contentual", as in carrying content beyond the symbols. From the same talk:
If we now begin to construct mathematics, we shall first set our sights upon elementary number theory; we recognize that we can obtain and prove its truths through contentual intuitive considerations. The formulas that we encounter when we take this approach are used only to impart information.
He is very clear that the justification for the use of formulas that are "just a symbols game" is that they are consistent with formulas that are contentual and are not just a symbols game. That is the debate between Hilbert and Brouwer, or formalism and intuitionism: whether or not all formulas must have an intuitive meaning ("content"). In formalism, not all of them must.
It is precisely because Hilbert's justification was based on consistency, as without it, "real" propositions could be wrong, that the incompleteness results made that justification unprovable.
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.
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.
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).
You can use equivalence relations and quotients w/ a computable foundation, you just need to rephrase what you mean by equality. See e.g. Kevin Buzzard's nice explanation at https://xenaproject.wordpress.com/2025/02/09/what-is-a-quoti...
Right, I'm aware you can, it's just much trickier to do it rigorously. But I suppose that may be more a comfort thing. Thanks for the link!
> 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 ⊢.
Gödel's incompleteness theorem tells you why it is a good idea to separate semantics (notion of truth) from syntax (reasoning). Because some things are true, although you cannot prove that they are.
Some people now put forward from this the idea that for the natural numbers we know, it is NOT either true or false if for example the twin prime conjecture holds. That is nonsense. It is just that our methods of proof are strictly weaker than our notion of truth is.
That this is so is not even surprising! It is a fact of life that what is true is not necessarily what you can prove to be true. Innocent people imprisoned are an example of that. Guilty people going free another. What is maybe surprising is that what is true in what we perceive as the "real world" is also true in mathematics, which we imagine to be an "ideal realm". But mathematics is ALSO part of the "real world"; if you understand this, it is not so surprising. Yes, I am a platonist, and I think that everybody who isn't is just plain wrong and confused.
Intensional functions are just a special case of extensional functions. Where extensional functions are defined on mathematical objects, intensional functions are extensional functions defined on representations of mathematical objects (which are also mathematical objects, by the way), but pretend to be acting on the mathematical objects themselves, not their representations. That is really all there is to it, it is not a deep philosophical mystery. To do so can of course be very useful!
> there is a single countable list that includes all things that might possibly have any mathematical existence at all.
Help me understand that. Isn't the Cantor diagonialization argument a proof that such a list cannot exist because, supposing it did exist, it could be used to construct an object not on the list? Are you proposing that your list somehow defeats Cantor here?
(Of course, we're using the word "list" loosely here. What we mean is a total function with domain Nat, right?)
Please see my comment at https://news.ycombinator.com/item?id=44271589 for my explanation.
> 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.
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?
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.
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.
- 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.
I would suggest Bishop’s Constructive Analysis.
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
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?
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.
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?
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
There arguably has been a failure of communication between type theorists and "traditional" mathematicians, but Buzzard unfortunately has a bit of a history of vocally spreading less-than-accurate information about type theory. I'd suggest not focusing too much on this one person's opinions and engaging with the subject for yourself if it interests you.
It's also worth keeping in mind that mathematicians traditionally haven't cared too much about foundations, and are not necessarily the best people to ask about them; see Hilbert, Bourbaki and the scorning of logic¹. Among people who are interested in foundations (logicians, category theorists, computer scientists, philosophers, ...), there is a pretty clear consensus that HoTT is a major step forward; but of course it's not the kind of "step forward" with immediate, observable results. As David Madore puts it, you wouldn't cut the roots of an apple tree just because no apples grow there.
[1] https://web.archive.org/web/20210506180228if_/https://www.dp...
> but of course it's not the kind of "step forward" with immediate, observable results.
Nice, it looks like you agree with Kevin Buzzard's claim about HoTT in the presentation I linked above. While mathematicians as a whole have historically not cared all that much about the practicality of formal foundations, it's worth noting that Kevin Buzzard has quite some expertise in dealing with the Grothendieck-style fuzzy, informal reasoning about equality that happens to be a key motivation behind HoTT itself and the univalence approach. What he seems to claim on the topic is that HoTT makes it a tiny bit easier to phrase a formal treatment of these issues, but you still have to do all the really hard work of proving that everything "respects" the equalities you claim it respects. The fact that you can then "transport" mathematical objects, proofs etc. along equalities is nifty but is also the kind of thing that would be glossed over to begin with in any informal treatment, so there's no real gain wrt. that.
In podcasts or open conversation he is far more critical of HoTT.
Do you have a reference for that, such as a podcast link? His paper on Grothendieck's use of equality is implicitly rather critical of HoTT proponents' claims anyway (which is why I linked that too), but I'm curious to know if he has publicly said anything more specific than that.
Go to 2:04:00 at https://www.youtube.com/watch?v=0zBDNYRfdlU
> Constructivism is a cancer in my view.
Thanks for the reference! That take of his sounds a bit confused in-context (univalence and constructivism are not directly related, you can work non-constructively and still use the overall featureset of HoTT/univalence) but then his remark about how he's just working on non-constructive stuff that we don't even know how to phrase constructively is just fair.
Relatedly, the kind of philosophical constructivism that would make claims like "non-constructive mathematics is just wrong and useless" has been a bit problematic in many ways, he's not totally off-base about this.
I disliked his skepticism about proofs-as-programs the most, but that's because I think "a direct proof is a program" is very much a worthwhile statement. Of course some mathematicians will opt not to care about that.
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.)
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.
> 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.
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.
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.
Can you really reassemble them into something bigger or just into more copies of the same size?
I've never quite gotten the axiom of choice. Can anyone ELI5?
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.
> 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)]`.
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.
The two statements imply each other, they are logically equivalent:
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.
> A human cannot describe said element, by definition.
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
> 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.
> 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.
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.)
> 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?
Well, you’d need some model of index, for one. And I’m not sure how you’d construct that with uncountably many elements. Even ignoring that, a set containing n elements is different from a set containing n sets of one element each.
Not saying your formulation is wrong, just that there’s a fair amount of non-obvious work to get to the classic formulation.
> Even ignoring that, a set containing n elements is different from a set containing n sets of one element each.
Different in what way? A set containing n sets of one element each is a set containing n elements.
In ZF, everything that's an element of a set is itself a set, so unless what's bothering you is the idea that "a set containing n elements" might contain the empty set, or a set with two elements, I'm not seeing it.
> you’d need some model of index, for one. And I’m not sure how you’d construct that with uncountably many elements
Why would the number of elements matter? Set elements aren't indexed. What are you using your model of index for?
I really feel I should repeat the question I asked you to begin with: You say you need to convert a Cartesian product into a set containing "its elements". In your mind, what is a Cartesian product, before that conversion takes place?
Okay, let’s simplify. Do we agree that the Cartesian product (a,b,c,a) is represented in ZFC as {{1 a} {2 b} {3 c} {4 d}} and that that is different from {a b c a}?
No. We don't.
Let's note first of all that (a, b, c, a) is a tuple, not a Cartesian product.
Where are you getting your ideas from? What do you think a Cartesian product is? Give me a definition.
Ok, I see your problem now. Tuples aren’t axiomatic components of set theory. Try proving they exist then you’ll see the problem too.
Well, it's true that tuples aren't defined by the ZF axioms. They do have a conventional definition, which you appear not to know.†
Natural numbers also aren't defined by the ZF axioms; why do you think that the definition of a tuple should involve them? You're likely to have a hard time finding a textbook that agrees.
I'm getting an overwhelming sense here that you don't know the meaning of the things you say. If you don't know what a Cartesian product is, why do you think it makes sense to talk about what you can and can't do with it?
Why do you think it makes sense to write {a b c a}, which has no meaning?
† For reference: by the standard convention, the tuple (a, b, c, a) is represented as the set {{{a, {a, b}}, {{a, {a, b}}, c}}, {{{a, {a, b}}, {{a, {a, b}}, c}, a}}. You might notice that no numbers appear anywhere. You might also notice that regardless of representation - and you're free to use other representations - it will never be a Cartesian product, because "tuple" and "Cartesian product" refer to different things.
Isn't that equivalent (or, ok, similar) to saying that we can decide undecidable mathematical truths?
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.
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.]
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)
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.
[0] https://en.wikipedia.org/wiki/Well-ordering_theorem
The single most best definition I know is what is on the wiki[0]:
> A choice function (also called selector or selection) is a function f, defined on a collection X of nonempty sets, such that for every set A in X, f(A) is an element of A. With this concept, the axiom can be stated:
> Axiom—For any set X of nonempty sets, there exists a choice function f that is defined on X and maps each set of X to an element of that set.
I like this definition because IMO it is simple, close to the name of the axiom, and you might want to use it in this form, that is, having a set of sets, and taking a choice function on them.
To understand its importance and the controversies around it, you'll need some examples and counterexamples how truthness and provability and knowability (regarding structures, numbers, metamathematics) interact; also what are the views of the majority of working mathematicians and people in other fields using mathematics.
[0] : https://en.wikipedia.org/wiki/Axiom_of_choice#Statement
Tangential, but a choice function is one of the ur-examples of Dependent Type Theory (DTT). In standard ZFC the choice function on X would have the type signature
And you know the additional information that (∀A:X) (f(A) ∈ A), which is not encoded in the type signature, just an additional fact that you know, and have to keep track of it. In DTT the codomain can be the function of the picked element of the domain. In this case, the DTT type signature of f would be So in this case the signature of the function carries strictly more information than in the case of normal, static function type signatures in ZFC. And the axiom of choice simply states that the type (A:X) -> A is non-empty if every A are non-empty.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...)
Not like 5, but High-school Geometry.
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).
Note that this proof doesn't require the axiom of choice, only excluded middle.
AC is much stronger than excluded middle. This doesn't really say anything about what AC does.
If you have a set of sets, you can pick one element from each set to construct another set.
This is provable if everything’s finite, but not if you’re dealing with things with bigger cardinalities like the real numbers.
This set of slides, originally devised for the Chaos Communication Congress, might be helpful: https://www.speicherleck.de/iblech/stuff/ac-38c3.pdf
- 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
Yes. Here’s a great ELI5 intro:
https://youtu.be/_cr46G2K5Fo?si=Q6iEm3m-Nyge3FUW
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).
The material is way over my head, but, wow, what a beautifully designed page. The layout and typography is delightful.
Thanks! The source code is set in Fabrizio Schiavi’s amazing PragmataPro.
https://fsd.it/shop/fonts/pragmatapro/
https://github.com/fabrizioschiavi/pragmatapro
[flagged]
[flagged]
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.
It is not about real world, choosing an axiom set must simply put produce something valid (with no contradictions) and that is not trivial.
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.
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.
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.