Live data from Hacker News

List of Statements Independent of ZFC

en.wikipedia.org

81–90 of 108 posts

Re: List of Statements Independent of ZFC

#81
post #58
post #46

Earlier quoted context omitted.

[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 clea…

Well done. Has anyone named a set in between the rationals and the reals?

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.

Re: List of Statements Independent of ZFC

#82
post #24

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.

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.

Re: List of Statements Independent of ZFC

#83
post #3

A very interesting discussion about this topic that also includes many examples and references is available on MathOverflow: 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 i…

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

Re: List of Statements Independent of ZFC

#84
post #51

Earlier quoted context omitted.

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?

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

Re: List of Statements Independent of ZFC

#85

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 val…

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.

Re: List of Statements Independent of ZFC

#86

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 val…

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…

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.

Re: List of Statements Independent of ZFC

#87
post #24

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.

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.

Re: List of Statements Independent of ZFC

#88
post #66

Earlier quoted context omitted.

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 ex…

>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.

So what practical applications do these functions have whose derivatives can't be approximated numerically ?

Re: List of Statements Independent of ZFC

#89
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...

Re: List of Statements Independent of ZFC

#90

Earlier quoted context omitted.

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 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 pro…

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.
Post reply on HN