Live data from Hacker News

List of Statements Independent of ZFC

en.wikipedia.org

91–100 of 108 posts

Re: List of Statements Independent of ZFC

#91
"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

Re: List of Statements Independent of ZFC

#92
post #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…

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/

Re: List of Statements Independent of ZFC

#93
post #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…

"The Axiom of Choice is obviously true, the Well–ordering theorem is obviously false; and who can tell about Zorn’s Lemma?"

Re: List of Statements Independent of ZFC

#94
post #46

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

Not OP but this was really well written. Thanks!

Re: List of Statements Independent of ZFC

#95
post #13
post #12

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

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.

Re: List of Statements Independent of ZFC

#96

Earlier quoted context omitted.

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.

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.

Re: List of Statements Independent of ZFC

#97
post #71

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

Re: List of Statements Independent of ZFC

#98

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.

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.

Re: List of Statements Independent of ZFC

#99

Earlier quoted context omitted.

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.

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.

Re: List of Statements Independent of ZFC

#100
post #88

Earlier quoted context omitted.

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

Probably lots in physics, aerospace, electrical engineering.

And, again, coming up with derived theorems that are useful.

Post reply on HN