Talk:Independence from ZFC: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
(Simplify →‎ZF vs. ZFC)
 
Line 9: Line 9:
:: 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 <math>N_{ZF} = N_{ZFC} = N_{ZF-Regularity}</math>? 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? [[User:Sligocki|Sligocki]] ([[User talk:Sligocki|talk]]) 21:24, 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 <math>N_{ZF} = N_{ZFC} = N_{ZF-Regularity}</math>? 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? [[User:Sligocki|Sligocki]] ([[User talk:Sligocki|talk]]) 21:24, 21 July 2025 (UTC)


::: I can say <math>N_{ZF} = N_{ZFC}</math> with confidence, since the statements that a TM halts and runs forever are <math>\Sigma^0_1</math> and <math>\Pi^0_1</math> respectively, and by [https://en.wikipedia.org/wiki/Absoluteness_(logic)#Shoenfield's_absoluteness_theorem Shoenfield's absoluteness theorem] ZF proves a <math>\Sigma^0_1</math> statement iff ZFC proves it, and same for <math>\Pi^0_1</math> 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 [https://en.wikipedia.org/wiki/Permutation_model permutation models] (also see [https://en.wikipedia.org/wiki/Axiom_of_regularity#Regularity_and_the_rest_of_ZF(C)_axioms]), but I don't know how to work with those so I can't say anything about <math>N_{ZF-Regularity}</math> unfortunately [[User:C7X|C7X]] ([[User talk:C7X|talk]]) 00:06, 22 July 2025 (UTC)
::: I can say <math>N_{ZF} = N_{ZFC}</math> with confidence, since the statement that a TM runs forever is <math>\Pi^0_1</math> respectively, and by [https://en.wikipedia.org/wiki/Absoluteness_(logic)#Shoenfield's_absoluteness_theorem Shoenfield's absoluteness theorem] ZF proves a <math>\Pi^0_1</math> 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 [https://en.wikipedia.org/wiki/Permutation_model permutation models] (also see [https://en.wikipedia.org/wiki/Axiom_of_regularity#Regularity_and_the_rest_of_ZF(C)_axioms]), but I don't know how to work with those so I can't say anything about <math>N_{ZF-Regularity}</math> unfortunately [[User:C7X|C7X]] ([[User talk:C7X|talk]]) 00:06, 22 July 2025 (UTC)

Latest revision as of 00:07, 22 July 2025

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 ? 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 with confidence, since the statement that a TM runs forever is respectively, and by Shoenfield's absoluteness theorem ZF proves a 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 unfortunately C7X (talk) 00:06, 22 July 2025 (UTC)