Talk:Independence from ZFC

A good introduction can come from here: https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-undecidability-bb748.pdf,

ZF vs. ZFC

The way this article is written makes it unclear what specifically applies for ZF vs. ZFC. I don't know the specifics myself, so some clarification would be nice. XnoobSpeakable

Currently, all of the machines listed in this article except one are written to start enumerating theorems of ZF-Regularity and halt if they find a contradiction, so they halt iff Con(ZF-Regularity) is false. Con(ZF-Regularity) is equivalent to Con(ZF) although I don't know how to prove that, but I do know how to prove that Con(ZF) is equivalent to Con(ZFC): if you assume ZF is consistent, there is a model of it, then you take the constructible universe of that model to obtain a model of ZFC, so then ZFC is consistent. The one different machine is the original Aaronson-Yedidia machine. Instead it uses one of Friedman's statements, which is independent of both ZF and ZFC (and even ZFC+some large cardinals!) C7X (talk) 20:04, 21 July 2025 (UTC)

Interesting, I didn't realize these were for ZF minus Axiom of Regularity. Looks like Wikipedia has some sources for Axiom of Regularity being "relatively consistent" with the rest of ZF: https://en.wikipedia.org/wiki/Axiom_of_regularity#Regularity_and_the_rest_of_ZF(C)_axioms although I haven't tried to read any of them. I suppose the motivation to remove regularity is just that it makes the TMs smaller since they have fewer axioms to enumerate? Does it sound correct to say that $N_{ZF}=N_{ZFC}=N_{ZF-Regularity}$? I guess maybe that is not known, but all the current TMs halt iff Con(ZF-Regularity) is false, so then are upper bounds for all three of these numbers? Sligocki (talk) 21:24, 21 July 2025 (UTC)

I can say $N_{ZF}=N_{ZFC}$ with confidence, since the statements that a TM halts and runs forever are $\Sigma _{1}^{0}$ and $\Pi _{1}^{0}$ respectively, and by Shoenfield's absoluteness theorem ZF proves a $\Sigma _{1}^{0}$ statement iff ZFC proves it, and same for $\Pi _{1}^{0}$ statements and much more. (This theorem is proven via pretty much the same trick that I mentioned above, passing to the constructible universe of a given model of ZF to obtain choice.) For ZF without regularity, the standard machinery used in work there seems to be working with permutation models (also see [1]), but I don't know how to work with those so I can't say anything about $N_{ZF-Regularity}$ unfortunately C7X (talk) 00:06, 22 July 2025 (UTC)