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 statement that a TM runs forever is ${\mathrm{\Pi }}_1^0$ respectively, and by Shoenfield's absoluteness theorem ZF proves a ${\mathrm{\Pi }}_1^0$ statement iff ZFC proves it. (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)

Extensionality

Could there be future progress made by removing the axiom of extensionality from the machines?

Z minus extensionality is equiconsistent with Z, but ZF minus extensionality is also equiconsistent with Z. (R. O. Gandy, "On the Axiom of Extensionality") Both of these theories still have regularity though, so it would still have to be checked that this result holds when replacement is removed. Gandy says that the reason replacement becomes weak is because y = z becomes hard to prove without extensionality, so maybe using collection instead could get its consistency strength back up to ZFC's. C7X (talk) 07:58, 6 November 2025 (UTC)