Talk:Logical independence - Revision history

Tlonuqbar: Tlonuqbar moved page Talk:Independence from ZFC to Talk:Logical independence: expanding scope

2026-02-11T22:06:24Z

Tlonuqbar moved page Talk:Independence from ZFC to Talk:Logical independence: expanding scope

← Older revision		Revision as of 22:06, 11 February 2026
(No difference)

C7X: /* Extensionality */

2025-11-06T07:59:45Z

Extensionality

← Older revision		Revision as of 07:59, 6 November 2025
Line 14:		Line 14:
	Would removing the axiom of extensionality from the machines be helpful for shrinking them further?		Would removing the axiom of extensionality from the machines be helpful for shrinking them further?

	Z minus extensionality is equiconsistent with Z, but ZF minus extensionality is also equiconsistent with Z. (R. O. Gandy, "[https://doi.org/10.2307/2271630 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. [[User:C7X\|C7X]] ([[User talk:C7X\|talk]]) 07:58, 6 November 2025 (UTC)		Z minus extensionality is equiconsistent with Z, but ZF minus extensionality is also equiconsistent with Z. (R. O. Gandy, "[https://doi.org/10.2307/2271630 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 without extensionality is because y = z occurs in the statement of replacement, so maybe using collection instead could get its consistency strength back up to ZFC's. [[User:C7X\|C7X]] ([[User talk:C7X\|talk]]) 07:58, 6 November 2025 (UTC)

C7X: /* Extensionality */

2025-11-06T07:59:16Z

Extensionality

← Older revision		Revision as of 07:59, 6 November 2025
Line 12:		Line 12:

	== Extensionality ==		== Extensionality ==
	~~Could there be future progress made by~~ removing the axiom of extensionality from the machines?		Would removing the axiom of extensionality from the machines be helpful for shrinking them further?

	Z minus extensionality is equiconsistent with Z, but ZF minus extensionality is also equiconsistent with Z. (R. O. Gandy, "[https://doi.org/10.2307/2271630 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. [[User:C7X\|C7X]] ([[User talk:C7X\|talk]]) 07:58, 6 November 2025 (UTC)		Z minus extensionality is equiconsistent with Z, but ZF minus extensionality is also equiconsistent with Z. (R. O. Gandy, "[https://doi.org/10.2307/2271630 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. [[User:C7X\|C7X]] ([[User talk:C7X\|talk]]) 07:58, 6 November 2025 (UTC)

C7X: /* ZF vs. ZFC */

2025-11-06T07:58:53Z

ZF vs. ZFC

← Older revision		Revision as of 07:58, 6 November 2025
Line 10:		Line 10:

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

			== 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, "[https://doi.org/10.2307/2271630 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. [[User:C7X\|C7X]] ([[User talk:C7X\|talk]]) 07:58, 6 November 2025 (UTC)

C7X: Simplify /* ZF vs. ZFC */

2025-07-22T00:07:44Z

Simplify ZF vs. ZFC

← Older revision		Revision as of 00:07, 22 July 2025
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)

C7X: /* ZF vs. ZFC */

2025-07-22T00:07:06Z

ZF vs. ZFC

← Older revision		Revision as of 00:07, 22 July 2025
Line 8:		Line 8:

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

Sligocki at 21:24, 21 July 2025

2025-07-21T21:24:46Z

← Older revision		Revision as of 21:24, 21 July 2025
Line 6:		Line 6:

	: 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!) [[User:C7X\|C7X]] ([[User talk:C7X\|talk]]) 20:04, 21 July 2025 (UTC)		: 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!) [[User:C7X\|C7X]] ([[User talk: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 <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)

C7X: /* ZF vs. ZFC */

2025-07-21T20:04:53Z

ZF vs. ZFC

← Older revision		Revision as of 20:04, 21 July 2025
Line 4:		Line 4:

	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. [[User:XnoobSpeakable\|XnoobSpeakable]]		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. [[User:XnoobSpeakable\|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!) [[User:C7X\|C7X]] ([[User talk:C7X\|talk]]) 20:04, 21 July 2025 (UTC)

XnoobSpeakable: add name, because it somehow is not there

2025-07-21T08:09:46Z

add name, because it somehow is not there

← Older revision		Revision as of 08:09, 21 July 2025
Line 3:		Line 3:
	== ZF vs. ZFC ==		== 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.		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. [[User:XnoobSpeakable\|XnoobSpeakable]]

XnoobSpeakable: /* ZF vs. ZFC */ new section

2025-07-21T08:07:39Z

ZF vs. ZFC: new section

← Older revision		Revision as of 08:07, 21 July 2025
Line 1:		Line 1:
	A good introduction can come from here: https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-undecidability-bb748.pdf,		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.