Return to Answer

Build a second machine $N$. $N$ searches for a proof in ZFC of, "if $N$ halts then $M$ halts". If it finds one, it halts.

ZFC can argue as follows. "Suppose $N$ halts. Then it found a proof that if $N$ halts then $M$ halts. This, combined with the trace of $N$ halting, would be a ZFC a proof that $M$ halts. Thus $M$ finds this and halts."

That paragraph is a ZFC proof that if $N$ halts then $M$ halts… which $N$ finds, so $N$ halts. Thus, by the same logic as above, there is a proof that $M$ halts, which it will find and then halt on.

Isn't this hilarious? We prove this fact about our self-referential machine by constructing a second self-referential machine. This is basically how the proof of Löb's theorem works (see Joel David Hamkins's answer).

Build a second machine $N$. $N$ searches for a proof in ZFC of, "if $N$ halts then $M$ halts". If it finds one, it halts.

ZFC can argue as follows. "Suppose $N$ halts. Then it found a proof that if $N$ halts then $M$ halts. This, combined with the trace of $N$ halting, would be a ZFC proof that $M$ halts. Thus $M$ finds this and halts."

That paragraph is a ZFC proof that if $N$ halts then $M$ halts… which $N$ finds, so $N$ halts. Thus, by the same logic as above, there is a proof that $M$ halts, which it will find and then halt on.

Isn't this hilarious? We prove this fact about our self-referential machine by constructing a second self-referential machine. This is basically how the proof of Löb's theorem works (see Joel David Hamkins's answer).

Build a second machine $N$. $N$ searches for a proof in ZFC of, "if $N$ halts then $M$ halts". If it finds one, it halts.

ZFC can argue as follows. "Suppose $N$ halts. Then it found a proof that if $N$ halts then $M$ halts. This, combined with the trace of $N$ halting, would be a ZFC a proof that $M$ halts. Thus $M$ finds this and halts."

That paragraph is a ZFC proof that if $N$ halts then $M$ halts… which $N$ finds, so $N$ halts. Thus, by the same logic as above, there is a proof that $M$ halts, which it will find and then halt on.

Isn't this hilarious? We prove this fact about our self-referential machine by constructing a second self-referential machine. This is basically how the proof of Löb's theorem works (see Joel David Hamkins's answer.)

Build a second machine $N$. $N$ searches for a proof in ZFC of, "if $N$ halts then $M$ halts". If it finds one, it halts.

ZFC can argue as follows. "Suppose $N$ halts. Then it found a proof that if $N$ halts then $M$ halts. This, combined with the trace of $N$ halting, would be a ZFC a proof that $M$ halts. Thus $M$ finds this and halts."

That paragraph is a ZFC proof that if $N$ halts then $M$ halts… which $N$ finds, so $N$ halts. Thus, by the same logic as above, there is a proof that $M$ halts, which it will find and then halt on.

Isn't this hilarious? We prove this fact about our self-referential machine by constructing a second self-referential machine. This is basically how the proof of Löb's theorem works (see Joel David Hamkins's answer).

Build a second machine $N$. $N$ searches for a proof in ZFC of, "if $N$ halts then $M$ halts". If it finds one, it halts.

ZFC can argue as follows. "Suppose $N$ halts. Then it found a proof that if $N$ halts then $M$ halts. This, combined with the trace of $N$ halting, would be a ZFC a proof that $M$ halts. Thus $M$ finds this and halts."

Thus there is a ZFC proof that if $N$ halts then $M$ halts… which $N$ finds, so $N$ halts. Thus, by the same logic as above, there is a proof that $M$ halts, which it will find and then halt on.

Isn't this hilarious? We prove this fact about our self-referential machine by constructing a second self-referential machine. This is basically how the proof of Löb's theorem works (see Joel David Hamkins's answer.)

Build a second machine $N$. $N$ searches for a proof in ZFC of, "if $N$ halts then $M$ halts". If it finds one, it halts.

ZFC can argue as follows. "Suppose $N$ halts. Then it found a proof that if $N$ halts then $M$ halts. This, combined with the trace of $N$ halting, would be a ZFC a proof that $M$ halts. Thus $M$ finds this and halts."

That paragraph is a ZFC proof that if $N$ halts then $M$ halts… which $N$ finds, so $N$ halts. Thus, by the same logic as above, there is a proof that $M$ halts, which it will find and then halt on.

Isn't this hilarious? We prove this fact about our self-referential machine by constructing a second self-referential machine. This is basically how the proof of Löb's theorem works (see Joel David Hamkins's answer.)