Talk:Logical independence - Revision history

Δ⁵: /* Why we should be more cautious regarding LLM-generated designs */

2026-10-14T14:07:59Z

Why we should be more cautious regarding LLM-generated designs

← Older revision		Revision as of 14:07, 14 October 2026
Line 8:		Line 8:

	: If this result is uncertain, most of the other results up to this point are as well, as they have no formalization, and have not had that much attention placed on verifying their correctness. None of these results have undergone rigorous peer review. Perhaps it would be in the interest of the community to write a human-reviewed paper detailing the project? [[User:Tlonuqbar\|Tlonuqbar]] ([[User talk:Tlonuqbar\|talk]]) 06:22, 14 October 2026 (UTC)		: If this result is uncertain, most of the other results up to this point are as well, as they have no formalization, and have not had that much attention placed on verifying their correctness. None of these results have undergone rigorous peer review. Perhaps it would be in the interest of the community to write a human-reviewed paper detailing the project? [[User:Tlonuqbar\|Tlonuqbar]] ([[User talk:Tlonuqbar\|talk]]) 06:22, 14 October 2026 (UTC)

			::Maybe; human-generated results are a result of intuitive analysis that comes from understanding how machines behave, not a result of alien optimisation processes, so they're inherently more trustworthy IMO. But yeah, there's a reason the BB 5 result had to go through peer review [[User:Δ⁵\|Δ⁵]] ([[User talk:Δ⁵\|talk]]) 14:07, 14 October 2026 (UTC)

	== ZF vs. ZFC ==		== ZF vs. ZFC ==

Tlonuqbar: correcting my grammar

2026-10-14T06:24:53Z

correcting my grammar

← Older revision		Revision as of 06:24, 14 October 2026
Line 5:		Line 5:
	There have been a recent formalisation of the claimed 254-state independent-from-ZFC TM. Although most would think that settles all doubts of validity, we need to remember that LLMs are not like us humans. They are not intelligent designers; they are much more similar to the blind idiot god of evolution. And the blind idiot god is well-known for disregarding all concerns except for the metric. LLMs have been known to exploit imperceptible bugs in other proof assistants before; without anyone who understands how the machine works, can we really say for sure that it actually does what the LLM says it does? Even if it is truly independent from ZFC, if we keep taking LLM-generated proofs at face value, we would be no better than a student who guesses his teacher's password without a hint of understanding. We would become p-zombies. [[User:Δ⁵\|Δ⁵]] ([[User talk:Δ⁵\|talk]]) 06:16, 14 October 2026 (UTC)		There have been a recent formalisation of the claimed 254-state independent-from-ZFC TM. Although most would think that settles all doubts of validity, we need to remember that LLMs are not like us humans. They are not intelligent designers; they are much more similar to the blind idiot god of evolution. And the blind idiot god is well-known for disregarding all concerns except for the metric. LLMs have been known to exploit imperceptible bugs in other proof assistants before; without anyone who understands how the machine works, can we really say for sure that it actually does what the LLM says it does? Even if it is truly independent from ZFC, if we keep taking LLM-generated proofs at face value, we would be no better than a student who guesses his teacher's password without a hint of understanding. We would become p-zombies. [[User:Δ⁵\|Δ⁵]] ([[User talk:Δ⁵\|talk]]) 06:16, 14 October 2026 (UTC)

	: I am very open to discussion about when ~~are where~~ to include these results and the use of AI in mathematics. For the record, I explicitly waited until a formalization was provided to include this.		: I am very open to discussion about when, if and how to include these results, and generally about the use of AI in mathematics. For the record, I explicitly waited until a formalization was provided to include this.

	: If this result is uncertain, most of the other results up to this point are as well, as they have no formalization, and have not had that much attention placed on verifying their correctness. None of these results have undergone rigorous peer review. Perhaps it would be in the interest of the community to write a human-reviewed paper detailing the project? [[User:Tlonuqbar\|Tlonuqbar]] ([[User talk:Tlonuqbar\|talk]]) 06:22, 14 October 2026 (UTC)		: If this result is uncertain, most of the other results up to this point are as well, as they have no formalization, and have not had that much attention placed on verifying their correctness. None of these results have undergone rigorous peer review. Perhaps it would be in the interest of the community to write a human-reviewed paper detailing the project? [[User:Tlonuqbar\|Tlonuqbar]] ([[User talk:Tlonuqbar\|talk]]) 06:22, 14 October 2026 (UTC)

Tlonuqbar: my opinions on this

2026-10-14T06:22:58Z

my opinions on this

← Older revision		Revision as of 06:22, 14 October 2026
Line 4:		Line 4:

	There have been a recent formalisation of the claimed 254-state independent-from-ZFC TM. Although most would think that settles all doubts of validity, we need to remember that LLMs are not like us humans. They are not intelligent designers; they are much more similar to the blind idiot god of evolution. And the blind idiot god is well-known for disregarding all concerns except for the metric. LLMs have been known to exploit imperceptible bugs in other proof assistants before; without anyone who understands how the machine works, can we really say for sure that it actually does what the LLM says it does? Even if it is truly independent from ZFC, if we keep taking LLM-generated proofs at face value, we would be no better than a student who guesses his teacher's password without a hint of understanding. We would become p-zombies. [[User:Δ⁵\|Δ⁵]] ([[User talk:Δ⁵\|talk]]) 06:16, 14 October 2026 (UTC)		There have been a recent formalisation of the claimed 254-state independent-from-ZFC TM. Although most would think that settles all doubts of validity, we need to remember that LLMs are not like us humans. They are not intelligent designers; they are much more similar to the blind idiot god of evolution. And the blind idiot god is well-known for disregarding all concerns except for the metric. LLMs have been known to exploit imperceptible bugs in other proof assistants before; without anyone who understands how the machine works, can we really say for sure that it actually does what the LLM says it does? Even if it is truly independent from ZFC, if we keep taking LLM-generated proofs at face value, we would be no better than a student who guesses his teacher's password without a hint of understanding. We would become p-zombies. [[User:Δ⁵\|Δ⁵]] ([[User talk:Δ⁵\|talk]]) 06:16, 14 October 2026 (UTC)

			: I am very open to discussion about when are where to include these results and the use of AI in mathematics. For the record, I explicitly waited until a formalization was provided to include this.

			: If this result is uncertain, most of the other results up to this point are as well, as they have no formalization, and have not had that much attention placed on verifying their correctness. None of these results have undergone rigorous peer review. Perhaps it would be in the interest of the community to write a human-reviewed paper detailing the project? [[User:Tlonuqbar\|Tlonuqbar]] ([[User talk:Tlonuqbar\|talk]]) 06:22, 14 October 2026 (UTC)

	== ZF vs. ZFC ==		== ZF vs. ZFC ==

Δ⁵ at 06:16, 14 October 2026

2026-10-14T06:16:01Z

← Older revision		Revision as of 06:16, 14 October 2026
Line 3:		Line 3:
	== Why we should be more cautious regarding LLM-generated designs ==		== Why we should be more cautious regarding LLM-generated designs ==

	There have been a recent formalisation of the claimed 254-state independent-from-ZFC TM. Although most would think that settles all doubts of validity, we need to remember that LLMs are not like us humans. They are not intelligent designers; they are much more similar to the blind idiot god of evolution. And the blind idiot god is well-known for disregarding all concerns except for the metric. LLMs have been known to exploit imperceptible bugs in other proof assistants before; without anyone who understands how the machine works, can we really say for sure that it actually does what the LLM says it does? Even if it is truly independent from ZFC, if we keep taking LLM-generated proofs at face value, we would be no better than a student who guesses his teacher's password without a hint of understanding. We would become p-zombies.		There have been a recent formalisation of the claimed 254-state independent-from-ZFC TM. Although most would think that settles all doubts of validity, we need to remember that LLMs are not like us humans. They are not intelligent designers; they are much more similar to the blind idiot god of evolution. And the blind idiot god is well-known for disregarding all concerns except for the metric. LLMs have been known to exploit imperceptible bugs in other proof assistants before; without anyone who understands how the machine works, can we really say for sure that it actually does what the LLM says it does? Even if it is truly independent from ZFC, if we keep taking LLM-generated proofs at face value, we would be no better than a student who guesses his teacher's password without a hint of understanding. We would become p-zombies. [[User:Δ⁵\|Δ⁵]] ([[User talk:Δ⁵\|talk]]) 06:16, 14 October 2026 (UTC)

	== ZF vs. ZFC ==		== ZF vs. ZFC ==

Δ⁵: A word of caution

2026-10-14T06:15:00Z

A word of caution

← Older revision		Revision as of 06:15, 14 October 2026
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,

			== Why we should be more cautious regarding LLM-generated designs ==

			There have been a recent formalisation of the claimed 254-state independent-from-ZFC TM. Although most would think that settles all doubts of validity, we need to remember that LLMs are not like us humans. They are not intelligent designers; they are much more similar to the blind idiot god of evolution. And the blind idiot god is well-known for disregarding all concerns except for the metric. LLMs have been known to exploit imperceptible bugs in other proof assistants before; without anyone who understands how the machine works, can we really say for sure that it actually does what the LLM says it does? Even if it is truly independent from ZFC, if we keep taking LLM-generated proofs at face value, we would be no better than a student who guesses his teacher's password without a hint of understanding. We would become p-zombies.

	== ZF vs. ZFC ==		== ZF vs. ZFC ==

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)