Eliezer made this attempt at naming a large number computable by a small Turing machine. What I’m wondering is exactly what axioms we need to use in order to prove that this Turning machine does indeed halt. The description of the Turing machine uses a large cardinal axiom (“there exists an I0 rank-into-rank cardinal”), but I don’t think that assuming this cardinal is enough to prove that the machine halts. Is it enough to assume that this axiom is consistent? Or is something stronger needed?
I used to be quite good at math at high school, but I haven’t studied it afterwards. This seems like a good opportunity to ask: Which book(s) should I read in order to fully understand that post?
Assume great knowledge of high-school math, but almost nothing beyond that. I want to get from there to… understanding the cardinals and ordinals. I have a vague impression of what they likely are, but I’d like to have a solid foundation, i.e. to know the definitions and to understand the proofs (in ideal case, to be able to prove some things independently).
Bonus points if the books you mention are available at Library Genesis. ;)
As well as ordinals and cardinals, Eliezer’s construction also needs concepts from the areas of computability and formal logic. A good book to get introduced to these areas is Boolos’ “Computability and Logic”.
Two good first books on set theory (with a similar scope) are
H. B. Enderton, Elements of Set Theory
Karel Hrbacek, Thomas Jech, Introduction to Set Theory
(Though they might be insufficient to parse the post.)
Keep in mind that set theory has a very different character from most math, so it might be better to turn to something else first if “studying math” is more of a motivation.
The only step in which his machine can fail to halt is “Run all programs such that a halting proof exists, until they halt.”. A program would have to have a halting proof, yet not halt. Therefore, beyond what we need to talk about turing machines at all, the only extra axiom needed is "T is consistent.".
Consistency of T isn’t enough, is it? For example the theory (PA + “The program that searches for a contradiction in PA halts”) is consistent, even though that program doesn’t halt.
I don’t follow. I agree that (PA + “PA is inconsistent”) is consistent. How does it follow that consistency of T isn’t enough? The way I use consistency there is “If T proves that a program halts, then that program does halt and we can safely run it.”.
I’m arguing that, for a theory T and Turing machine P, “T is consistent” and “T proves that P halts” aren’t together enough to deduce that P halts. And as I counter example I suggested T = PA + “PA is inconsistent” and P = “search for an inconsistency in PA”. This P doesn’t halt even though T is consistent and proves it halts.
So if it doesn’t work for that T and P, I don’t see why it would work for the original T and P.
I thought of that before but I was a bit worried about it because Löb’s Theorem says that a theory can never prove this axiom schema about itself. But I think we’re safe here because we’re assuming “If T proves φ, then φ” while not actually working in T.
Eliezer made this attempt at naming a large number computable by a small Turing machine. What I’m wondering is exactly what axioms we need to use in order to prove that this Turning machine does indeed halt. The description of the Turing machine uses a large cardinal axiom (“there exists an I0 rank-into-rank cardinal”), but I don’t think that assuming this cardinal is enough to prove that the machine halts. Is it enough to assume that this axiom is consistent? Or is something stronger needed?
I used to be quite good at math at high school, but I haven’t studied it afterwards. This seems like a good opportunity to ask: Which book(s) should I read in order to fully understand that post?
Assume great knowledge of high-school math, but almost nothing beyond that. I want to get from there to… understanding the cardinals and ordinals. I have a vague impression of what they likely are, but I’d like to have a solid foundation, i.e. to know the definitions and to understand the proofs (in ideal case, to be able to prove some things independently).
Bonus points if the books you mention are available at Library Genesis. ;)
As well as ordinals and cardinals, Eliezer’s construction also needs concepts from the areas of computability and formal logic. A good book to get introduced to these areas is Boolos’ “Computability and Logic”.
Thank you!
Two good first books on set theory (with a similar scope) are
H. B. Enderton, Elements of Set Theory
Karel Hrbacek, Thomas Jech, Introduction to Set Theory
(Though they might be insufficient to parse the post.)
Keep in mind that set theory has a very different character from most math, so it might be better to turn to something else first if “studying math” is more of a motivation.
Thank you!
The only step in which his machine can fail to halt is “Run all programs such that a halting proof exists, until they halt.”. A program would have to have a halting proof, yet not halt.
Therefore, beyond what we need to talk about turing machines at all, the only extra axiom needed is"T is consistent.".Consistency of T isn’t enough, is it? For example the theory (PA + “The program that searches for a contradiction in PA halts”) is consistent, even though that program doesn’t halt.
I don’t follow. I agree that (PA + “PA is inconsistent”) is consistent. How does it follow that consistency of T isn’t enough? The way I use consistency there is “If T proves that a program halts, then that program does halt and we can safely run it.”.
I’m arguing that, for a theory T and Turing machine P, “T is consistent” and “T proves that P halts” aren’t together enough to deduce that P halts. And as I counter example I suggested T = PA + “PA is inconsistent” and P = “search for an inconsistency in PA”. This P doesn’t halt even though T is consistent and proves it halts.
So if it doesn’t work for that T and P, I don’t see why it would work for the original T and P.
Right. Perhaps the axiom schema “If T proves φ, then φ.”?
Yeah, I think that’s probably right.
I thought of that before but I was a bit worried about it because Löb’s Theorem says that a theory can never prove this axiom schema about itself. But I think we’re safe here because we’re assuming “If T proves φ, then φ” while not actually working in T.