List of Statements Independent of ZFC(en.wikipedia.org)
en.wikipedia.org
List of Statements Independent of ZFC
https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC
107 comments
So, does that mean that one can assume this to be true and build a perfectly consistent theory, or conversely assume it to be false (with - say - at least one counter-example) and build another perfectly consistent theory?
Yes, this is the exact meaning of “independent from” here.
[deleted]
Well, it's not possible to prove the consistency, thanks to Godel. Maybe one of your new theories would contain a statement, inconsistent with the rest of ZFC.
When we say that a statement P is independent of ZFC what we're really saying is "if ZFC is consistent, then P is independent of ZFC (hence both ZFC+P and ZFC+not P are consistent)".
This is the only sensible way to interpret claims of independency, since if ZFC is inconsistent it just proves every statement so there's no independent ones
This is the only sensible way to interpret claims of independency, since if ZFC is inconsistent it just proves every statement so there's no independent ones
This is incorrect. It absolutely is possible to prove consistency, what Gödel tells us is that in any consistent logic system there are true but unprovable (in that system) statements.
For this particular list, the statements have been proven to both be consistent with ZFC and for their negations to be consistent with ZFC.
For this particular list, the statements have been proven to both be consistent with ZFC and for their negations to be consistent with ZFC.
This is first incompleteness theorem. What deepsun was referring to is second incompleteness theorem - in a consistent system F the statement 'F is consistent' is in fact unprovable (in F).
It gets worse than that, by Easton's theorem, except for two mild restrictions provable on ZFC, the function that sends a regular cardinal to the cardinality of its powerset can be anything
That is a strange one.
Infinities are strange.
Try thinking about how you could probe that the integers have fewer subsets than the reals using ZFC.
That still feels intuitive. Like for any open interval there are uncountably many reals and a finite number of integers. It seems like nothing changes as you expand the interval.
The integers HAVE fewer subsets than the reals!
Cantor's theorem tells us that the power set of any set has more elements than said set. It's also well known that the reals have the same cardinality as the power set of the integers.
Therefore, |P(R)| > |R| = |P(N)| > |N|, so the power set of the reals has more elements than the power set of integers.
The continuous hypothesis is the belief that no cardinal exists between |N| and |P(N)|. My previous argument fails if we pick two sets A and B, such that |A| < |B| < |P(A)|.
Therefore, |P(R)| > |R| = |P(N)| > |N|, so the power set of the reals has more elements than the power set of integers.
The continuous hypothesis is the belief that no cardinal exists between |N| and |P(N)|. My previous argument fails if we pick two sets A and B, such that |A| < |B| < |P(A)|.
[deleted]
sansnomme(2)
WTF I'm pretty sure I can prove that
It is easy to prove for finite sets (just count) but much harder for infinite ones. For example, which has more subsets, the integers or the positive integers? How about the integers and the reals?
If you answered "the integers" to the first question, you aren't thinking about this right, as the integers and the positive integers have the same number of elements to start with. source: https://en.wikipedia.org/wiki/Aleph_number
If you answered "the integers" to the first question, you aren't thinking about this right, as the integers and the positive integers have the same number of elements to start with. source: https://en.wikipedia.org/wiki/Aleph_number
Another example of why mathematics are a wrong abstraction to be optimally useful.
Mathematics should have bounds in the same way as our universe has bounds.
Any theorem that has a different behavior if something is infinite doesn't matter at all and is a waste of time for real engineers who solve things in the real world. The niche of mathematics that describe things beyond what our universe has to offer should be an optional extension to the mathematical framework instead of being the default, in order to not pollute discussions.
This is a fine and defensible (although not mainstream) viewpoint with several adherents among mathematicians and various levels of success in making it formal and precise.
See e.g. https://en.wikipedia.org/wiki/Finitism
Doron Zeilberger would like to pat you on the back.
See e.g. https://en.wikipedia.org/wiki/Finitism
Doron Zeilberger would like to pat you on the back.
Since you feel so strongly about it, let me argue that you're simply wrong:
Infinities have the opposite effect then you might think, they make things simpler. It's much easier to reason about an infinite list of numbers then to reason about 64 bit numbers.
In analysis, it's much easier to reason about infinitely differentiable, or smooth, surfaces then very rigid and complicated services.
The fact that infinities cause some complications in the foundations itself is a drop in the bucket to the practical application and simplifications of day to day mathematics.
Infinities have the opposite effect then you might think, they make things simpler. It's much easier to reason about an infinite list of numbers then to reason about 64 bit numbers.
In analysis, it's much easier to reason about infinitely differentiable, or smooth, surfaces then very rigid and complicated services.
The fact that infinities cause some complications in the foundations itself is a drop in the bucket to the practical application and simplifications of day to day mathematics.
> Infinities have the opposite effect then you might think, they make things simpler. It's much easier to reason about an infinite list of numbers then to reason about 64 bit numbers.
I would argue that a few extra lines in a proof is a small price to pay to avoid the Godelian catastrophe.
I would argue that a few extra lines in a proof is a small price to pay to avoid the Godelian catastrophe.
A formalist might say that mathematics has no infinities. Even infinite sets are just definitions of finite length, even if expanded all the way to ZFC axioms. The problem is your intuitive understanding.
A realist might say that mathematics exists within this universe, therefore it is equally subject to its constraints just like anything else. Problems arise via misapplication or misinterpretation of the math.
A model theorist might point out that even in models of math with only a countable collection of objects, it's still true that the reals are uncountable. The problem isn't with infinitie, it's that the finitary objects have subtle interactions.
A logician might object that ZFC already does start of with an intuitive notion of infinity, i.e. the counting numbers is a natural collection. The problem is that this inevitably has unintended consequences.
A historian might gently point out that this debate already occurred vigorously about 150 years ago, and the verdict was that we just gotta live with the weirdness of infinities. The problem is that we lose too much useful math by trying to throw them out.
Etc.
A realist might say that mathematics exists within this universe, therefore it is equally subject to its constraints just like anything else. Problems arise via misapplication or misinterpretation of the math.
A model theorist might point out that even in models of math with only a countable collection of objects, it's still true that the reals are uncountable. The problem isn't with infinitie, it's that the finitary objects have subtle interactions.
A logician might object that ZFC already does start of with an intuitive notion of infinity, i.e. the counting numbers is a natural collection. The problem is that this inevitably has unintended consequences.
A historian might gently point out that this debate already occurred vigorously about 150 years ago, and the verdict was that we just gotta live with the weirdness of infinities. The problem is that we lose too much useful math by trying to throw them out.
Etc.
Yes, my current inclination would be to define truth (in a practical sense) as that which is computable. Everything else belongs to the realm of fiction or fantasy.
Note that I don't mean to imply that this is the entirety of my philosophy. Just that one should distinguish between what is practically relevant and what is not and I think the current state of mathematics and CS does a poor job of making this distinction.
Note that I don't mean to imply that this is the entirety of my philosophy. Just that one should distinguish between what is practically relevant and what is not and I think the current state of mathematics and CS does a poor job of making this distinction.
The most prolific contemporary proponent of this view is probably Norman Wildberger, who takes a very unconventional approach and tries to build everything without real numbers, which he doesn't believe make physical or logical sense and therefore shouldn't be used as a basis for anything.
He's very nearly a minority of one, mind you.
He's very nearly a minority of one, mind you.
Tell all of the engineers using calculus that they don't need infinity.
And you can't easily only partially include infinity.
And you can't easily only partially include infinity.
Computers handle calculus quite nicely using numerical algorithms, which don't involve any infinite sets.
> And you can't easily only partially include infinity.
Sure you can. You just need to use a dx that's small enough for the particular functions you're working with and the degree of precision you need.
> And you can't easily only partially include infinity.
Sure you can. You just need to use a dx that's small enough for the particular functions you're working with and the degree of precision you need.
Calculus would likely not be invented without infinity. Many theorems, identities, and techniques may be approximated but ultimately rely on proofs using infinities - I doubt we would have discovered them quickly or at all without infinity. After all, the very concept of a limit evokes the concept of an infinite sequence.
That is true historically but I doubt that it is true necessarily. I mean I suspect that starting from what we now know it should be possible to reconstruct calculus (at least for all practical purposes) without reference to infinities or infinitesimals.
One argument in favor of this belief is that neither practical computations nor analytic intuition require actual infinitesimals.
The later, at least, has been my experience. I think I have a fairly decent practical intuition for calculus based on imagining dx becoming smaller and smaller until it's small enough, but I don't think my brain has any actual representation of "true infinitesimals" and my intuition breaks down completely if I try to imagine things like the relationship between the rational and irrational numbers. Maybe that's due to my intellectual limitations, but I wonder if it isn't because these concepts might be over-elaborate abstractions that don't really exist in our world.
One argument in favor of this belief is that neither practical computations nor analytic intuition require actual infinitesimals.
The later, at least, has been my experience. I think I have a fairly decent practical intuition for calculus based on imagining dx becoming smaller and smaller until it's small enough, but I don't think my brain has any actual representation of "true infinitesimals" and my intuition breaks down completely if I try to imagine things like the relationship between the rational and irrational numbers. Maybe that's due to my intellectual limitations, but I wonder if it isn't because these concepts might be over-elaborate abstractions that don't really exist in our world.
>One argument in favor of this belief is that neither practical computations nor analytic intuition require actual infinitesimals.
Don't derivatives count? That's a pretty important and trivial calculation. Sure, you can approximate it when it's nicely behaved, but they aren't always. There's also lots of verrrrrrry slowly converging series that can't be easily computed numerically.
Don't derivatives count? That's a pretty important and trivial calculation. Sure, you can approximate it when it's nicely behaved, but they aren't always. There's also lots of verrrrrrry slowly converging series that can't be easily computed numerically.
Except for all that numerical analysis around floating point arithmetic...
Could you give a use case?
All of calculus.
It's possible to do quite a lot without infinities in calculus and trigonometry, whether it makes sense to bother is another question.
https://en.m.wikipedia.org/wiki/Rational_trigonometry
https://en.m.wikipedia.org/wiki/Rational_trigonometry
> It's possible to do quite a lot without infinities in calculus and trigonometry
This is like Stacey King saying "I'll always remember this as the night that Michael Jordan and I combined for 70 points."
Pretty much the entire field of Analysis (of which calculus is a part) relies on 'infinities' of some kind. Even if you try to restrict to the rationals, you're still typically working with infinite series of them.
You can do some analysis over the rationals, but often this takes the form of Cauchy sequences of rationals which might be cheating.
[0] https://math.stackexchange.com/questions/387234/how-far-can-...
[1] https://www.dpmms.cam.ac.uk/~wtg10/reals.html
This is like Stacey King saying "I'll always remember this as the night that Michael Jordan and I combined for 70 points."
Pretty much the entire field of Analysis (of which calculus is a part) relies on 'infinities' of some kind. Even if you try to restrict to the rationals, you're still typically working with infinite series of them.
You can do some analysis over the rationals, but often this takes the form of Cauchy sequences of rationals which might be cheating.
[0] https://math.stackexchange.com/questions/387234/how-far-can-...
[1] https://www.dpmms.cam.ac.uk/~wtg10/reals.html
Being "optimally useful" is not the goal of mathematics. See for example, https://www.dpmms.cam.ac.uk/~wtg10/2cultures.pdf
I know that feeling. It never lasts long.
>I'm pretty sure I can prove that
For infinite sets of arbitrarily large cardinality?
For infinite sets of arbitrarily large cardinality?
No I can't.
But see my answer to correct_horse
I'm tempted to exclude the Axiom of Choice (AC) from any math I do, and instead include the Axiom of Determinacy (AD) [1] (which contradicts AC), so that all subsets of R^n are measurable [2] (thus precluding the Banach–Tarski paradox), and the Axiom of Dependent Choice (DC), which is weaker than AC but sufficient to develop most of real analysis. Like, I don't really care if not all vector spaces have a basis; it's enough for me that all interesting vector spaces do (I think).
But then we have this (from [3]):
> For each of the following statements, there is some model of ZF¬C where it is true:
> - In some model, there is a set that can be partitioned into strictly more equivalence classes than the original set has elements, and a function whose domain is strictly smaller than its range. In fact, this is the case in all known models.
So it's really, pick your own poison - either one of these:
- you can take apart a ball and put the pieces back together into two balls
- there exists a function whose range is larger than its domain
Math is weird.
[1] https://en.wikipedia.org/wiki/Axiom_of_determinacy
[2] https://en.wikipedia.org/wiki/Solovay_model
[3] https://en.wikipedia.org/wiki/Axiom_of_choice#Statements_con...
But then we have this (from [3]):
> For each of the following statements, there is some model of ZF¬C where it is true:
> - In some model, there is a set that can be partitioned into strictly more equivalence classes than the original set has elements, and a function whose domain is strictly smaller than its range. In fact, this is the case in all known models.
So it's really, pick your own poison - either one of these:
- you can take apart a ball and put the pieces back together into two balls
- there exists a function whose range is larger than its domain
Math is weird.
[1] https://en.wikipedia.org/wiki/Axiom_of_determinacy
[2] https://en.wikipedia.org/wiki/Solovay_model
[3] https://en.wikipedia.org/wiki/Axiom_of_choice#Statements_con...
In fact it's an open problem (very likely the oldest open problem in set theory) whether in every model of not AC there is a set with such a paradoxical partition! Here's a nice introduction to the problem by Asaf Karagila http://karagila.org/2014/on-the-partition-principle/
"The Axiom of Choice is obviously true, the Well–ordering theorem is obviously false; and who can tell about Zorn’s Lemma?"
Some of this was familiar, but I also saw this:
> In 1973, Saharon Shelah showed that the Whitehead problem ("is every abelian group A with Ext^1(A, Z) = 0 a free abelian group?") is independent of ZFC.
(This is the same Shelah who proved what is usually called "Sauer's Lemma" on set separability, upon which the "VC dimension" and the resulting VC learning theory are based.)
Anyway, this was surprising because I didn't know there were any theorems outside of set theory that had been known and studied, and then later turned out to be independent of ZFC.
Apparently, the surprise I felt is just because I wasn't paying attention -- there are a couple of other problems in the page that seem to have a similar flavor. I'm not enough of a mathematician to appreciate to what extent they are interesting problems that arise independently of counterexamples.
[edited to add: the comment of @triska nearby addresses exactly this point!]
> In 1973, Saharon Shelah showed that the Whitehead problem ("is every abelian group A with Ext^1(A, Z) = 0 a free abelian group?") is independent of ZFC.
(This is the same Shelah who proved what is usually called "Sauer's Lemma" on set separability, upon which the "VC dimension" and the resulting VC learning theory are based.)
Anyway, this was surprising because I didn't know there were any theorems outside of set theory that had been known and studied, and then later turned out to be independent of ZFC.
Apparently, the surprise I felt is just because I wasn't paying attention -- there are a couple of other problems in the page that seem to have a similar flavor. I'm not enough of a mathematician to appreciate to what extent they are interesting problems that arise independently of counterexamples.
[edited to add: the comment of @triska nearby addresses exactly this point!]
Another famous example of that kind is the existence of outer automorphisms of the Calkin algebra, which is a simple question about a naturally occuring object which turned out to be independent of ZFC by work of Farah and Weaver.
Topology and set theoretic topology is full of those statements, are there Suslin lines? Are there S-spaces? Is the product of two ccc spaces also ccc? The list goes on
Another one from analysis is a very strong form of Fubini's theorem that was shown independent by Friedman.
There's surely more but those are the ones I could remember right now!
Topology and set theoretic topology is full of those statements, are there Suslin lines? Are there S-spaces? Is the product of two ccc spaces also ccc? The list goes on
Another one from analysis is a very strong form of Fubini's theorem that was shown independent by Friedman.
There's surely more but those are the ones I could remember right now!
Is there any ELI5-type explanation for us non-mathers? Whenever I see stuff like this, I start trying to actually understand it, then fail miserably just trying to google terms I'm not familiar with. Is advanced knowledge of these math principles required to understand the significance of this page, or why it is interesting?
[The following isn't really "like you're five", but given how long it is already that's probably just as well.]
Proofs and formal systems, and why we're kinda screwed
Mathematicians like to prove things. What we would really like would be to be able to find, for every mathematical statement, either a proof that it's true or a proof that it's false.
It wasn't until the early 20th century that mathematicians got a clear enough idea of what proof is to figure out whether that could be done. And it turns out it can't! That was proved in 1931 by Kurt Goedel, who did something that these days is very familiar to anyone in computing but was novel then: he found a way to encode mathematical statements, and sequences of mathematical statements, as numbers, in such a way that properties of those statements turn into properties of the numbers, so that you can use ordinary mathematics to reason about them.
This enabled him to show that if you have any system for doing mathematics that (1) is powerful enough to describe ordinary arithmetical statements and (2) is simple enough that you can check mechanically what is and isn't a proof, then there are statements that that system can neither prove nor disprove. (With a proviso I'll come to in a couple of paragraphs.)
So much for the hopes of mathematicians.
Anyway, despite that setback, mathematicians didn't abandon the idea of building up all of mathematics in some nice simple formalized system in which we can prove and disprove things. We still like to do that, and have come to terms with the fact that there will be things we can neither prove nor disprove.
... Unless the system we're working in happens to be inconsistent, meaning that there's some proposition that it can both prove and disprove. In that case, what actually happens is that it can prove everything, which is of course completely useless. So far as we know, the systems we like to use aren't inconsistent. It would be nice to prove they aren't -- but there's a nice variant of Goedel's theorem that says not just "for any system that isn't inconsistent, there are propositions it can't decide" but "for any system that isn't inconsistent, a formalized statement of its own consistency is a proposition it can't decide".
Once, again, so much for the hopes of mathematicians.
The particular formal system called ZFC
One particular nice simple formalized system is called ZFC, which is short for "Zermelo-Fraenkel set theory with the Axiom of Choice". That's a bit of a mouthful. So, "set theory" means that the basic idea we're starting with is that of a set of things. (In order to do mathematics, we certainly need some idea like that. It turns out that taking it as the foundational idea works fairly well.) Zermelo was a mathematician who came up with one fairly good way to do that. Fraenkel was another mathematician who improved Zermelo's system.
The "Axiom of Choice" -- the C in ZFC -- is a rather technical statement in set theory that turns out to be (1) "obviously true" according to some mathematicians' intuition, (2) useful for proving things we care about, and (3) something that plain old ZF, without the C, can neither prove nor disprove. (Unless, as usual, ZF is actually inconsistent.) In particular, this means that if ZF is a consistent system -- if it isn't able to prove 1+1=3 -- then ZFC is as well. (Because if you could get a contradiction out of ZFC, you could use it to prove not-C within ZF.) So adding the Axiom of Choice to ZF is "safe"; it can't create contradictions that weren't already there. And, since it's useful, we tend to keep it around.
[You can skip the next two paragraphs if you like. They describe the sort of thing you do if you want to build up all of mathematics on top of set theory.]
So, how do you build mathematics out of set theory? The usual sort of game you play is this. We want to be able to talk about numbers. So first of all we find an implementation of numbers in terms of sets. (If you were doing mathematics in a computer you'd want to do roughly the reverse, and build your sets out of numbers.) So we might, e.g., say that 0 "is" the empty set, and then 1 "is" the set containing just 0, and then 2 "is" the set containing just 0 and 1, and so forth. That gets you a load of sets that can (as well as being sets) do double duty as the non-negative integers. Then you construct the integers (negative as well as positive) out of those, and then the rational numbers (ratios of integers) out of those, and then you need some fancier footwork to get the "real numbers" (including things like pi and the square root of 2).
And then you're off to the races, because once you have the real numbers you can do geometry: e.g., three-dimensional space "is" the set of triples (x,y,z) of real numbers, and things like spheres and dodecahedra are just sets of points in space. And now you have numbers and geometrical things, and you can build all the other weirder more abstract things mathematicians like to study in a similar way.
OK, so if we have sets then we have everything, so a formalized set theory is a reasonable thing to try to use as a basis for mathematics. But, ever since Goedel, we know that any formalized system will be unable to decide (i.e., either prove or disprove) some statements we might be interested in.
What that page is about
The Wikipedia page linked here is a list of statements we might be interested in that ZFC is, as it turns out, unable to decide. "Independent of" means "neither provable nor disprovable from".
(There are other systems you can use instead of ZFC. Some of them are other varieties of set theory; some work entirely differently. It usually turns out that you can translate most statements of ordinary mathematics to and fro between them, and that what's provable and what isn't doesn't depend on "implementation details" (e.g., I described one particular way to build non-negative integers out of sets; what if we do it a different way? The answer is usually that it doesn't matter). But some systems are "stronger" than others and can prove or refute more statements. To be usable for mathematics, a system can't be "too much" weaker than ZFC. And since in some sense ZFC encodes most of the things that mathematicians are pretty sure "ought" to be true, most systems people want to use aren't "too much" stronger than ZFC either. A lot of the statements on that page would also be on similar pages about systems other than ZFC.)
A lot of those statements are weird technical things that only a mathematician could care about, and indeed that only a mathematician specifically interested in what's provable from ZFC and what isn't could care about. Some of them are at least potentially interesting to some mathematicians for their own sake, but understanding them generally requires a pile of background that (1) I don't really have myself in most cases and (2) you really don't want me to make this long enough to deal with.
But here's one of them, one of the oldest of them all. Some sets are bigger than others. For instance, {1,2,3} is bigger than {1,2}. What about infinite sets? It's not obvious a priori what "bigger" should even mean for infinite sets, but Georg Cantor (a pioneer of this stuff) found a good answer, whose details we don't need right now. It turns out that the integers are "the same size" as the rational numbers, even though the integers seem like a tiny subset of the rational numbers, but that the real numbers are "bigger". So here's the question: are there any sets bigger than the rational numbers but smaller than the real numbers? This is called the "continuum hypothesis", which is a bit of a stupid name but never mind, and it is neither provable nor disprovable in ZFC.
Proofs and formal systems, and why we're kinda screwed
Mathematicians like to prove things. What we would really like would be to be able to find, for every mathematical statement, either a proof that it's true or a proof that it's false.
It wasn't until the early 20th century that mathematicians got a clear enough idea of what proof is to figure out whether that could be done. And it turns out it can't! That was proved in 1931 by Kurt Goedel, who did something that these days is very familiar to anyone in computing but was novel then: he found a way to encode mathematical statements, and sequences of mathematical statements, as numbers, in such a way that properties of those statements turn into properties of the numbers, so that you can use ordinary mathematics to reason about them.
This enabled him to show that if you have any system for doing mathematics that (1) is powerful enough to describe ordinary arithmetical statements and (2) is simple enough that you can check mechanically what is and isn't a proof, then there are statements that that system can neither prove nor disprove. (With a proviso I'll come to in a couple of paragraphs.)
So much for the hopes of mathematicians.
Anyway, despite that setback, mathematicians didn't abandon the idea of building up all of mathematics in some nice simple formalized system in which we can prove and disprove things. We still like to do that, and have come to terms with the fact that there will be things we can neither prove nor disprove.
... Unless the system we're working in happens to be inconsistent, meaning that there's some proposition that it can both prove and disprove. In that case, what actually happens is that it can prove everything, which is of course completely useless. So far as we know, the systems we like to use aren't inconsistent. It would be nice to prove they aren't -- but there's a nice variant of Goedel's theorem that says not just "for any system that isn't inconsistent, there are propositions it can't decide" but "for any system that isn't inconsistent, a formalized statement of its own consistency is a proposition it can't decide".
Once, again, so much for the hopes of mathematicians.
The particular formal system called ZFC
One particular nice simple formalized system is called ZFC, which is short for "Zermelo-Fraenkel set theory with the Axiom of Choice". That's a bit of a mouthful. So, "set theory" means that the basic idea we're starting with is that of a set of things. (In order to do mathematics, we certainly need some idea like that. It turns out that taking it as the foundational idea works fairly well.) Zermelo was a mathematician who came up with one fairly good way to do that. Fraenkel was another mathematician who improved Zermelo's system.
The "Axiom of Choice" -- the C in ZFC -- is a rather technical statement in set theory that turns out to be (1) "obviously true" according to some mathematicians' intuition, (2) useful for proving things we care about, and (3) something that plain old ZF, without the C, can neither prove nor disprove. (Unless, as usual, ZF is actually inconsistent.) In particular, this means that if ZF is a consistent system -- if it isn't able to prove 1+1=3 -- then ZFC is as well. (Because if you could get a contradiction out of ZFC, you could use it to prove not-C within ZF.) So adding the Axiom of Choice to ZF is "safe"; it can't create contradictions that weren't already there. And, since it's useful, we tend to keep it around.
[You can skip the next two paragraphs if you like. They describe the sort of thing you do if you want to build up all of mathematics on top of set theory.]
So, how do you build mathematics out of set theory? The usual sort of game you play is this. We want to be able to talk about numbers. So first of all we find an implementation of numbers in terms of sets. (If you were doing mathematics in a computer you'd want to do roughly the reverse, and build your sets out of numbers.) So we might, e.g., say that 0 "is" the empty set, and then 1 "is" the set containing just 0, and then 2 "is" the set containing just 0 and 1, and so forth. That gets you a load of sets that can (as well as being sets) do double duty as the non-negative integers. Then you construct the integers (negative as well as positive) out of those, and then the rational numbers (ratios of integers) out of those, and then you need some fancier footwork to get the "real numbers" (including things like pi and the square root of 2).
And then you're off to the races, because once you have the real numbers you can do geometry: e.g., three-dimensional space "is" the set of triples (x,y,z) of real numbers, and things like spheres and dodecahedra are just sets of points in space. And now you have numbers and geometrical things, and you can build all the other weirder more abstract things mathematicians like to study in a similar way.
OK, so if we have sets then we have everything, so a formalized set theory is a reasonable thing to try to use as a basis for mathematics. But, ever since Goedel, we know that any formalized system will be unable to decide (i.e., either prove or disprove) some statements we might be interested in.
What that page is about
The Wikipedia page linked here is a list of statements we might be interested in that ZFC is, as it turns out, unable to decide. "Independent of" means "neither provable nor disprovable from".
(There are other systems you can use instead of ZFC. Some of them are other varieties of set theory; some work entirely differently. It usually turns out that you can translate most statements of ordinary mathematics to and fro between them, and that what's provable and what isn't doesn't depend on "implementation details" (e.g., I described one particular way to build non-negative integers out of sets; what if we do it a different way? The answer is usually that it doesn't matter). But some systems are "stronger" than others and can prove or refute more statements. To be usable for mathematics, a system can't be "too much" weaker than ZFC. And since in some sense ZFC encodes most of the things that mathematicians are pretty sure "ought" to be true, most systems people want to use aren't "too much" stronger than ZFC either. A lot of the statements on that page would also be on similar pages about systems other than ZFC.)
A lot of those statements are weird technical things that only a mathematician could care about, and indeed that only a mathematician specifically interested in what's provable from ZFC and what isn't could care about. Some of them are at least potentially interesting to some mathematicians for their own sake, but understanding them generally requires a pile of background that (1) I don't really have myself in most cases and (2) you really don't want me to make this long enough to deal with.
But here's one of them, one of the oldest of them all. Some sets are bigger than others. For instance, {1,2,3} is bigger than {1,2}. What about infinite sets? It's not obvious a priori what "bigger" should even mean for infinite sets, but Georg Cantor (a pioneer of this stuff) found a good answer, whose details we don't need right now. It turns out that the integers are "the same size" as the rational numbers, even though the integers seem like a tiny subset of the rational numbers, but that the real numbers are "bigger". So here's the question: are there any sets bigger than the rational numbers but smaller than the real numbers? This is called the "continuum hypothesis", which is a bit of a stupid name but never mind, and it is neither provable nor disprovable in ZFC.
Not OP but this was really well written. Thanks!
Well done.
Has anyone named a set in between the rationals and the reals?
Has anyone named a set in between the rationals and the reals?
The canonical example is https://en.wikipedia.org/wiki/Vitali_set
You can kinda think of it as "the set of real numbers MOD the set of rationals". Kinda. And they're dorked up because the length is infinitesimal, but a countably infinite number of them add up to length 1.
For a more precise explanation see here: https://math.stackexchange.com/a/137959/287133
You can kinda think of it as "the set of real numbers MOD the set of rationals". Kinda. And they're dorked up because the length is infinitesimal, but a countably infinite number of them add up to length 1.
For a more precise explanation see here: https://math.stackexchange.com/a/137959/287133
Also note that the construction of the above set requires the axiom of choice. And, as we all know, the axiom of choice is equivalent to the continuum hypothesis in ZFC. So that's how it all fits.
Whether a set of cardinality strictly between the rationals and reals exists is independent of ZFC.
https://en.m.wikipedia.org/wiki/Continuum_hypothesis
There are many sets which are strict supersets of the rationals and strictly sheets of the reals, of course.
https://en.m.wikipedia.org/wiki/Continuum_hypothesis
There are many sets which are strict supersets of the rationals and strictly sheets of the reals, of course.
"strictly subsets of the reals", thanks autocorrect.
For example, if ℚ is the rationals and ℝ is the reals then ℚ∪{√2} is a strict superset of the rationals but a strict subset of the reals. However, it still has the same cardinality as the rationals (cf. https://en.wikipedia.org/wiki/Hilbert%27s_paradox_of_the_Gra...)
For example, if ℚ is the rationals and ℝ is the reals then ℚ∪{√2} is a strict superset of the rationals but a strict subset of the reals. However, it still has the same cardinality as the rationals (cf. https://en.wikipedia.org/wiki/Hilbert%27s_paradox_of_the_Gra...)
If the continuum hypothesis (CH) holds then there is none.
Assume that CH fails and well order the reals. An initial segment of length omega_1 is an example of such a set.
Assume that CH fails and well order the reals. An initial segment of length omega_1 is an example of such a set.
These are a list of theories that can’t be proven or disproven using the most common mathematical foundation.
I recall once I read the short book "The Philosophy of Set Theory" [1] since I like philosophy and have an interest in Math. It contains much of the history that lead up to the decision to base significant portions of the soundness of mathematics on top of set theory (and by proxy: Cantor's work on infinities). My recollection is fuzzy since it was years ago but I recall it starts at Zeno's paradox and follows along to calculus and beyond.
The book suggests there was a lot of displeasure and argumentation within the philosophy and math communities because it was felt that there was no real basis for infinitesimals. Some mathematicians (I believe Hilbert and Frege among them?) became determined to shut-up the pesky philosophers by proving the soundness of math based on some logical axiomatic fundamentals. Of course, this was later proven to be impossible by Gödel but at the time they considered it a win that philosophers and mathematicians could at least agree on logic (and more broadly "logical empiricism" which is a basis of "analytical philosophy").
I recall being completely dissatisfied at the arguments presented in favour of ZFC (not mathematically, but philosophically). I remember there was a single paragraph somewhere in the final third of the book that I head to re-read several times before I finally gave up in frustration. My impression of this history is that the mathematicians "won" in some sense by railroading their ideas. Calculus works, right? It is extremely effective and leads to correct results ... so ignore the seeming paradox of summing an infinite quantity of infinitesimally small values and move on already! Further, ignore the actual paradoxes inherent in infinite sets. And this was all done not because there was some problem to be solved but rather to shut-down debate that seemed to undermine the philosophical position of logical empiricism.
Another interesting (if historically questionable) exploration of this topic is the graphic novel Logicomix [2]. This work follows Bertrand Russel and Wittgenstein through this period in our history.
1. https://www.amazon.com/Philosophy-Set-Theory-Introduction-Ma...
2. https://en.wikipedia.org/wiki/Logicomix
The book suggests there was a lot of displeasure and argumentation within the philosophy and math communities because it was felt that there was no real basis for infinitesimals. Some mathematicians (I believe Hilbert and Frege among them?) became determined to shut-up the pesky philosophers by proving the soundness of math based on some logical axiomatic fundamentals. Of course, this was later proven to be impossible by Gödel but at the time they considered it a win that philosophers and mathematicians could at least agree on logic (and more broadly "logical empiricism" which is a basis of "analytical philosophy").
I recall being completely dissatisfied at the arguments presented in favour of ZFC (not mathematically, but philosophically). I remember there was a single paragraph somewhere in the final third of the book that I head to re-read several times before I finally gave up in frustration. My impression of this history is that the mathematicians "won" in some sense by railroading their ideas. Calculus works, right? It is extremely effective and leads to correct results ... so ignore the seeming paradox of summing an infinite quantity of infinitesimally small values and move on already! Further, ignore the actual paradoxes inherent in infinite sets. And this was all done not because there was some problem to be solved but rather to shut-down debate that seemed to undermine the philosophical position of logical empiricism.
Another interesting (if historically questionable) exploration of this topic is the graphic novel Logicomix [2]. This work follows Bertrand Russel and Wittgenstein through this period in our history.
1. https://www.amazon.com/Philosophy-Set-Theory-Introduction-Ma...
2. https://en.wikipedia.org/wiki/Logicomix
I’m not sure that any side won. ZFC is merely a game with clearly defined rules that lots of people have agreed to play, but it is not the only game, by a long stretch.
I think it feels easier to say that now that we are long past the point where the debates occurred. But this happened during a time when universities were still trying to figure out how to divide up sciences.
Nowadays, the idea that math has a role to play in pretty much every science isn't really questioned at all. I mean, imagine I suggested that something other than math should be brought to bear on physics. I doubt a single person in here would support such an approach on any level. I think that represents a clear win. Answering objections about the fundamentals of math using formalisms like ZFC was a component of that.
Nowadays, the idea that math has a role to play in pretty much every science isn't really questioned at all. I mean, imagine I suggested that something other than math should be brought to bear on physics. I doubt a single person in here would support such an approach on any level. I think that represents a clear win. Answering objections about the fundamentals of math using formalisms like ZFC was a component of that.
ZFC has very little to do with why math is used in universities or the sciences, and it would still be used even without it, because as you said, it works. It worked for 3000 years before we had ZFC after all.
ZFC wasn’t even the end of the debate on mathematical foundations even in math. There are a lot of people trying to redo everything with types and category theory today.
ZFC wasn’t even the end of the debate on mathematical foundations even in math. There are a lot of people trying to redo everything with types and category theory today.
ZFC follows along a path including (but not started by) Russell/Whiteheads Principia Mathematica, which famously (infamously?) takes several hundred pages to prove 1+1=2. I doubt very few have thought ZFC (or it's variants) would be the last word.
Almost no scientists cared about formalizing or proving the soundness of the mathematical tools they used. In the same way the majority of programmers do not care about proving the soundness of their programming languages. In general, people seem to be interested in the practical aspects of their work.
But the general idea that symbolic logic is the primary basis for understanding the world is something a bit different and something we rarely question now. I think people assume that this is some obvious thing but it is actually an idea that was coordinated and forwarded. It appears to me that the debate at the beginning of the 20th century around using set theory to establish the foundations of math by way of logic is when the scale seems to have heavily tipped towards that particular idea.
Almost no scientists cared about formalizing or proving the soundness of the mathematical tools they used. In the same way the majority of programmers do not care about proving the soundness of their programming languages. In general, people seem to be interested in the practical aspects of their work.
But the general idea that symbolic logic is the primary basis for understanding the world is something a bit different and something we rarely question now. I think people assume that this is some obvious thing but it is actually an idea that was coordinated and forwarded. It appears to me that the debate at the beginning of the 20th century around using set theory to establish the foundations of math by way of logic is when the scale seems to have heavily tipped towards that particular idea.
I can't speak for scientists, but programmers usually care very much about the soundness (not in the Curry-Howard sense) of their type systems.
I disagree and I'm sure we'd only be able to trade anecdotes and no real evidence. However, my experience working in industry for 20+ years is that almost no working programmers pay any attention to such things. For example, when my team recently decided to switch from Javascript to Typescript there was zero consideration about the fundamental soundness of either language. I had the same experience when a team I recently worked with was debating a switch from Java to Kotlin. Nothing approaching the topic of soundness even came up.
I think hacker news can be a bubble since these deeper issues can sometimes appear here. I recall a recent post about a soundness bug found in Rust and it generated quite a lot of discussion. However, I see that as analogous to the intense scrutiny of a small cabal of scientists/philosophers, the Vienna Circle for example, who did take these fundamentals seriously in math/sciences. I just do not believe and have not experienced that sentiment to be prevalent outside of this bubble.
I think hacker news can be a bubble since these deeper issues can sometimes appear here. I recall a recent post about a soundness bug found in Rust and it generated quite a lot of discussion. However, I see that as analogous to the intense scrutiny of a small cabal of scientists/philosophers, the Vienna Circle for example, who did take these fundamentals seriously in math/sciences. I just do not believe and have not experienced that sentiment to be prevalent outside of this bubble.
Why is it always zfc plus optionally something else? Is there anything other than zfc that creates an interesting starting point?
These are excellent questions! And yes, there is!
For example, I highly recommend the paper Rethinking set theory by Tom Leinster:
https://arxiv.org/abs/1212.6543
It highlights Lawvere set theory. The paper won this year's Chauvenet Prize:
https://www.maa.org/programs-and-communities/member-communit...
For example, I highly recommend the paper Rethinking set theory by Tom Leinster:
https://arxiv.org/abs/1212.6543
It highlights Lawvere set theory. The paper won this year's Chauvenet Prize:
https://www.maa.org/programs-and-communities/member-communit...
Isn't Lawvere set theory equiconsistent with bounded Zermelo set theory?
ZFC, its subtheories, and its extensions, serve as a universal yardstick for consistency results. It's not really clear why that is the case, but it has so far proven to be so.
ZFC, its subtheories, and its extensions, serve as a universal yardstick for consistency results. It's not really clear why that is the case, but it has so far proven to be so.
In other news, there's recently been a mechanized proof for one of the ZFC independent problems: https://flypitch.github.io/papers/
https://news.ycombinator.com/item?id=21823618
https://news.ycombinator.com/item?id=21823618
I love seeing pure math on HN. I think math is the purest expression of what it means to be curious. It sometimes gives us fun toys to build into whatever we are coding.
Hopefully this will clear at least some of the Gödelian misconceptions that pop up from time to time here
How? Misunderstandings about Gödel's theorem are unlikely to be due to a misunderstanding of the axioms of set theory (more likely of logical issues such as the technical meaning of 'incompleteness'), let alone to a lack of understanding of what statements are independent of a common set of axioms.
Which Gödel misconceptions?
One can write down a concrete polynomial p ∈ Z[x1,...x9] such that the statement "there are integers m1,...,m9 with p(m1,...,m9)=0" can neither be proven nor disproven in ZFC (assuming ZFC is consistent).
So you were to specify such a thing and the thing was small enough it's value could be determined by a command line program and you found integers m1.... m9 such that when you typed them at the command line, the value returned was 0, would "reality" have determined a "truth" that was not deducible?
Still, I can't see each of the steps wouldn't be easily determined by existing axioms.
Anyway, my head hurts.
So you were to specify such a thing and the thing was small enough it's value could be determined by a command line program and you found integers m1.... m9 such that when you typed them at the command line, the value returned was 0, would "reality" have determined a "truth" that was not deducible?
Still, I can't see each of the steps wouldn't be easily determined by existing axioms.
Anyway, my head hurts.
OK, the way I'd figure it out is: for such a polynomial, you definitely can't find those integers. There isn't any concrete m1...m9 satisfying the condition. The stumbling block is you can't find a proof for this fact in ZFC.
But this seems to go against the idea that for any proposition independent from an axiom system, there is a model of the axiom system where that proposition is true and another where it is false.
Someone enlighten me (not sarcastic).
But this seems to go against the idea that for any proposition independent from an axiom system, there is a model of the axiom system where that proposition is true and another where it is false.
Someone enlighten me (not sarcastic).
> OK, the way I'd figure it out is: for such a polynomial, you definitely can't find those integers. There isn't any concrete m1...m9 satisfying the condition. The stumbling block is you can't find a proof for this fact in ZFC.
If this were formalizable it would be a proof.
I encourage you to read through the excellent piece on the busy beaver function and computability. It's not entirely related, but it's fun! And it touches on the same theme as your question here, that human intuition about mathematics is weak. The writeup describes and proves the non-computability of a particular function of positive integers with definite (but non-computable!) value.
https://www.scottaaronson.com/writings/bignumbers.html
If this were formalizable it would be a proof.
I encourage you to read through the excellent piece on the busy beaver function and computability. It's not entirely related, but it's fun! And it touches on the same theme as your question here, that human intuition about mathematics is weak. The writeup describes and proves the non-computability of a particular function of positive integers with definite (but non-computable!) value.
https://www.scottaaronson.com/writings/bignumbers.html
> If this were formalizable it would be a proof.
A proof, but not a proof that can be expressed inside ZFC.
A proof, but not a proof that can be expressed inside ZFC.
Obviously, the original statement has been proved to be independent from ZFC.
You're right that if ZFC is consistent then it has a model in which this polynomial has an integer root. The issue is that the "integers" in the model are different from the actual integers. So you can't take the root out of the model and use it to prove ZFC inconsistent.
That is certainly how I would understand the situation.
However, it seems intuitively you construct the notion of finite, could engage in the ordinary computation and have a way of distinguishing these "weird roots" from regular roots.
I suppose if you make the position of (something like) "every polynomial whose root cannot be found by finite calculation does not, in fact, have one" an axiom but then you would have discarded the notion of finite axioms (you'd have a second order system).
Still, might actually have a way to specify "truth", something I'd thought was a bit beyond logic at this point.
However, it seems intuitively you construct the notion of finite, could engage in the ordinary computation and have a way of distinguishing these "weird roots" from regular roots.
I suppose if you make the position of (something like) "every polynomial whose root cannot be found by finite calculation does not, in fact, have one" an axiom but then you would have discarded the notion of finite axioms (you'd have a second order system).
Still, might actually have a way to specify "truth", something I'd thought was a bit beyond logic at this point.
You might be interested in https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo....
The point is that if ZFC is consistent then there are no such integers. So a computer program searching for them would run forever without returning any output. But since we can't prove that ZFC is consistent you would never know whether your computer program was really running for ever. Even after a million years you wouldn't be able to prove that it wouldn't finally give some output in five minutes time.
Consistency or inconsistency seems like a red herring here. The proposition concerns conjures independent of ZFC if ZFC is consistent.
Assuming is ZFC is consistent, the theory says there are polynomials whose zeros we could forever fruitless search for but which couldn't be proved to have no zeros in ZFC. We could forever fruitlessly search for a proof of the polynomail having no zero, in fact (putting it this way, returns the situation to something marginally understandable, in fact makes something that would follow from the halting problem).
If ZFC is inconsistent, we actually could prove that this polynomial had a zero and we could prove it didn't have a zero, since we could prove anything, at least anything in the vocabulary of ZFC.
Assuming is ZFC is consistent, the theory says there are polynomials whose zeros we could forever fruitless search for but which couldn't be proved to have no zeros in ZFC. We could forever fruitlessly search for a proof of the polynomail having no zero, in fact (putting it this way, returns the situation to something marginally understandable, in fact makes something that would follow from the halting problem).
If ZFC is inconsistent, we actually could prove that this polynomial had a zero and we could prove it didn't have a zero, since we could prove anything, at least anything in the vocabulary of ZFC.
What's a reasonable strategy of proving a statement like that is undecidable in ZFC?
I think it must use some tools I'm unfamiliar with.
I think it must use some tools I'm unfamiliar with.
[deleted]
Either you show that your statement P is equivalent to another known independent one or you need to produce a model of P and a model of not P.
The two main techniques to produce new models of ZFC are inner models, that is submodels of a model, for example studying the inner model L (Gödel's constructible universe) is how the consistency of the continuum hypothesis, the generalized continuum hypothesis, the existence of Suslin trees etc. was shown. Looking at L also allows one to conclude that the axiom of choice is consistent with ZF. Another commonly study inner model is the so called HOD, and there's a whole area, "inner model theory" that essentially tries to construct canonical inner models for some statements.
The second big way to produce a model of ZFC is by forcing. This is a very versatile tool that allows to extend a given model of ZFC by adding a new set to it (for example by adding a lot of new reals numbers to a model of CH you can make CH false). Forcing is how the consistency of the negation of CH and GCH was proved.
An interisting example is the negation of AC and its consistency with ZF. If you happen to live in a model of AC every forcing extension will still be a model of AC so it seems that our previous techniques are powerless. But actually what can be done is to look at a carefully chosen submodel of a forcing extension that still models ZF but in which AC fails.
The two main techniques to produce new models of ZFC are inner models, that is submodels of a model, for example studying the inner model L (Gödel's constructible universe) is how the consistency of the continuum hypothesis, the generalized continuum hypothesis, the existence of Suslin trees etc. was shown. Looking at L also allows one to conclude that the axiom of choice is consistent with ZF. Another commonly study inner model is the so called HOD, and there's a whole area, "inner model theory" that essentially tries to construct canonical inner models for some statements.
The second big way to produce a model of ZFC is by forcing. This is a very versatile tool that allows to extend a given model of ZFC by adding a new set to it (for example by adding a lot of new reals numbers to a model of CH you can make CH false). Forcing is how the consistency of the negation of CH and GCH was proved.
An interisting example is the negation of AC and its consistency with ZF. If you happen to live in a model of AC every forcing extension will still be a model of AC so it seems that our previous techniques are powerless. But actually what can be done is to look at a carefully chosen submodel of a forcing extension that still models ZF but in which AC fails.
There are 2 popular ways.
1.Set-theoretic technique : forcing, e.g. Cohen forcing which was used in the proof of the independence of the continuum hypothesis.A good reference is Shelah's book on forcing.
2. Model-theoretic: construct a model for ZFC in which the negation of the statement is true and another model for which the statement is true.
There may be proof-theoretic techniques based on the non-existence of proofs involving finitely many steps, but I am not aware of these.
1.Set-theoretic technique : forcing, e.g. Cohen forcing which was used in the proof of the independence of the continuum hypothesis.A good reference is Shelah's book on forcing.
2. Model-theoretic: construct a model for ZFC in which the negation of the statement is true and another model for which the statement is true.
There may be proof-theoretic techniques based on the non-existence of proofs involving finitely many steps, but I am not aware of these.
Since ZFC can't prove its own consistency, you can't actually prove any statement is independent (an inconsistent system proves everything). Instead what is proved is that if ZFC is consistent then the statment is independent. There's a theorem called Gödel's completeness theorem (a somewhat confusing name in the light of his more famous incompleteness theorem, but they talk about different things so there's no conflict between them) that says that a system is consistent if and only if there exists a model of that system. So the way that you normally prove "If ZFC is consistent then S is independent" is by assuming ZFC is consistent, using the Completeness Theorem to show that it has a model, altering that model to produce models of ZFC+S and ZFC+¬S, and then using the Completeness Theorem in the other direction to conclude that both ZFC+S and ZFC+¬S are consistent.
To show that a sentence P is independent of a theory (that is, a set of sentences) T, generally one constructs or demonstrates the existence of a model of T + P and also produces a model of T + (not P).
https://en.wikipedia.org/wiki/Model_theory
https://en.wikipedia.org/wiki/Model_theory
Show that it implies the consistency of ZFC, and that its negation also does so. Or show that it's equivalent to a statement that's already on that list.
I believe it is what is called metalogical proofs
"The mathematical statements discussed below are provably independent of ZFC (the canonical axiomatic set theory of contemporary mathematics, consisting of the Zermelo–Fraenkel axioms plus the axiom of choice), assuming that ZFC is consistent. A statement is independent of ZFC (sometimes phrased "undecidable in ZFC") if it can neither be proven nor disproven from the axioms of ZFC."
- TFA
- TFA
"ZFC" is an esoteric acronym; I posted the quote from the article to help others because the title was entirely opaque to me.
Might something like this be fscking unification in physics?
I doubt it. Physics doesn’t seem to have much which is clearly connected to proof systems.
And, besides, from any (consistent) axiom system for which a given statement is undecidable, there is another axiom system which is the same except it adds that statement as an additional axiom, and the statement is therefore (trivially) provable in that system.
And, it doesn’t seem like physics is constrained to use only some specific axiom system.
It seems to me that the relevant thing to physics would be, rather than an axiom system, instead, a model (in the math sense, not the physics sense).
And, besides, from any (consistent) axiom system for which a given statement is undecidable, there is another axiom system which is the same except it adds that statement as an additional axiom, and the statement is therefore (trivially) provable in that system.
And, it doesn’t seem like physics is constrained to use only some specific axiom system.
It seems to me that the relevant thing to physics would be, rather than an axiom system, instead, a model (in the math sense, not the physics sense).
Thanks.
But doesn't that lead to systems with infinite numbers of axioms?
But doesn't that lead to systems with infinite numbers of axioms?
If you want to add axioms in order to be able to show each of an infinite number of statements which are all independent of the initial axiom system, and also none of them follow from the rest of them, that could involve an infinite set of axioms, yes,
but any statement we could make about stuff in physics, if it could be expressed in the language of the formal system, would, as a single statement, be something that could be added as a single axiom.
but any statement we could make about stuff in physics, if it could be expressed in the language of the formal system, would, as a single statement, be something that could be added as a single axiom.
What are some reasonable-sounding statements that are independent of ZFC?
https://mathoverflow.net/questions/1924/what-are-some-reason...
With the top voted result currently being:
"If a set X is smaller in cardinality than another set Y, then X has fewer subsets than Y."
As is also mentioned in the linked entry, this statement is independent of ZFC.