I just wanted to contribute a barnacle answer to user21820's monumental post above, in particular an intuition relating to the Barber paradox I first wrote about here. My hope is that my answer here explains how to use the Barber paradox to motivate most of the constructions in user21820's answer.
Barber paradox: consider a person $B$ defined as follows: $B$ shaves all and only the people who do not shave themselves. I.e. $B$ is s.t. on input $P$ (a person),
$$\begin{aligned} &\text{Def. }B(P): \\ & |\quad \text{if $P$ shaves $P$:}\\ & |\quad|\quad \text{$B$ $\neg$shaves $P$.}\\ & |\quad \text{if $P$ $\neg$shaves $P$:}\\ & |\quad|\quad \text{$B$ shaves $P$.}\\ \end{aligned}$$ QUESTION: But then does $B$ shave $B$? The conclusion of this Barber paradox is that this definition doesn't make sense, and such a Barber $B$ can not exist.
Halting contrarian paradox: consider a 1-input program $\sf{Contrarian}$ defined as follows: $\sf{Contrarian}$ halts-on ($\downarrow$) all and only the 1-input programs who do not halt-on themselves. I.e. $\sf{Contrarian}$ is s.t. on input $\tt s$ (the source code of a 1-input program $P_{\tt s}$),
$$\begin{aligned} &\text{Def. }\textsf{Contrarian}(\mathtt s): \\ & |\quad \text{if $P_{\tt s}(\mathtt s)\downarrow$:} &\color{gray}{(\text{if $P_{\tt s}$ halts on input $\tt s$...})}\\ & |\quad|\quad \uparrow. & \color{gray}{(\text{...then run forever ($\uparrow$)})}\\ & |\quad \text{if $P_{\tt s}(\mathtt s)\uparrow$:}\\ & |\quad|\quad \downarrow. \\ \end{aligned}$$ QUESTION: But then does $\textsf{Contrarian}$ halt on input $\tt{Contrarian}$ (its own source code)? The conclusion of this Halting contrarian paradox is that this definition doesn't make sense, and such a 1-input program $\sf{Contrarian}$ can not exist.
(The issue is that a computer can not compute whether or not $P_{\tt s}(\mathtt s)\downarrow$. I.e. if there was an algorithm to decide the Halting Problem, then $\sf{Contrarian}$ would be a valid computer program. Because we've shown $\sf{Contrarian}$ can not be a valid program, we conclude that the Halting Problem must be incomputable)
Ok, now we make a version of $\sf{Contrarian}$, that is definitely computable.
Fix a formal system $T$ (in language $\mathscr L$), with a proof verifier (as in user21820's answer) $V(\varphi, x)$ --- which I will notate as $(T \vdash^{(x)} \varphi)\checkmark$ --- a computer program that "decides (halts and answers) whether $x$ is a $T$-proof of $\varphi$".
Example: $T$ is PA --- Peano axioms with classical logic, and the Verifier program takes in a string comprised of the symbols $\mathscr L_\text{Peano} := \{v_1,\ldots, (, ), =, <, >, \neg, \land, \lor, \exists, \forall, +, \cdot, 0, 1\}$, and checks whether or not that string can be read as a sequence of logical sentences connected by logical rules, like modus ponens).
- It is a fact that statements like "this is the activity log of a program/Turing machine running for this many steps" can be encoded in Peano arithmetic, see https://www.cmi.ac.in/~madhavan/courses/pl2024/lectures/RecursiveFunctionsAndTMs.pdf (some more context here)
$$\begin{aligned} &\text{Def. }\textsf{ComputableContrarian}(\mathtt s): \\ & |\quad\text{lex-run through $\mathscr L$-strings } x: \\ & |\quad|\quad \text{if $(T \vdash^{(x)} P_{\tt s}(\mathtt s)\downarrow)\checkmark$:} &\color{gray}{(\text{if $x$ is a $T$-proof that $P_{\tt s}$ halts on input $\tt s$...})}\\ & |\quad|\quad|\quad \uparrow. & \color{gray}{(\text{...then run forever ($\uparrow$)})}\\ & |\quad|\quad \text{if $(T \vdash^{(x)} P_{\tt s}(\mathtt s)\uparrow)\checkmark$:}\\ & |\quad|\quad|\quad \downarrow. \\ \end{aligned}$$ ("lex-run through $\mathscr L$-strings $x$: {...}" means to start with the empty string $x$, perform the steps inside the {...}, then increment $x$ to the next simplest string using the symbols in $\mathscr L$, and so forth. For example for binary strings, we start with $x$ is empty, then $0, 00, 01, 10, 11, 000, 001, \ldots$)
QUESTION: But then does $\textsf{ComputableContrarian}$ halt on input $\tt{ComputableContrarian}$ (its own source code)?
I define the 0-input program $\textsf{B}$ (named in honor of "barber") as $$\textsf{B} := \textsf{ComputableContrarian}(\tt{ComputableContrarian})$$ The QUESTION is then "does $\sf B \downarrow$?", or written out in full: does the following program halt: $$\begin{aligned} & \text{lex-run through $\mathscr L$-strings } x:\\ & |\quad \text{if $(T \vdash^{(x)} {\sf B}\downarrow)\checkmark$:} \\ & |\quad|\quad \uparrow. \\ & |\quad \text{if $(T \vdash^{(x)} {\sf B}\uparrow)\checkmark$:}\\ & |\quad|\quad \downarrow. \\ \end{aligned}$$
Before we think about whether $\sf B \downarrow$ is true or not, let's think about whether or not there is a $T$-proof of it, or its negation. We $\color{red}{\textbf{assume}}$ that $T$ is consistent, and can reason about programs (as defined by user21820).
| Suppose f.s.o.c. $\sf B \downarrow$ is $T$-provable. | Suppose f.s.o.c. $\sf B \uparrow$ is $T$-provable. |
|---|---|
| Then there is a shortest $T$-proof $p$ of "$\sf B\downarrow$". | Then there is a shortest $T$-proof $q$ of "$\sf B\uparrow$". |
| Then, if we press play on the program $\sf B$ (whose full code I wrote out above), lexrun will find $p$ and enter the 1st "if" (unless lexrun never made it to $p$ because there was a proof $q<p$ of "$\sf B\uparrow$"; but in this case $T$ proves both $\sf B\downarrow$ and $\sf B\uparrow$, contradicting that $T$ is $\color{red}{\textbf{assumed}}$ consistent) | Then, if we press play on the program $\sf B$ (whose full code I wrote out above) lexrun will find $q$ and enter the 2nd "if" (unless lexrun never made it to $q$ because there was a proof $p<q$ of "$\sf B\downarrow$"; but in this case $T$ proves both $\sf B\uparrow$ and $\sf B\downarrow$, contradicting that $T$ is $\color{red}{\textbf{assumed}}$ consistent) |
| Entering the 1st "if" means that $\sf B\uparrow$ (truly, if we were to run this program on a real-world computer) | Entering the 2nd "if" means that $\sf B\downarrow$ (truly, if we were to run this program on a real-world computer) |
| $T$ can go through the finitely many strings $< p$, and verify that they are NOT proofs of "$\sf B\uparrow$", and then recognize that $p$ is a proof of "$\sf B\downarrow$", and hence deduce that if one were to press play on the program $\sf B$, the 1st "if" would be entered first, leading to $\sf B$ playing on forever ($\uparrow$). | ... |
| The previous paragraph can be formalized into a $T$-proof $q$ (necessarily $q>p$) of "$\sf B\uparrow$". But then again $T$ can prove both $\sf B\uparrow$ and $\sf B\downarrow$, contradicting that $T$ is $\color{red}{\textbf{assumed}}$ consistent. | ... |
Congrats! We've just proved the Gödel-Rosser 1st incompleteness theorem, and gave an extremely explicit example of a sentence (namely, "$\sf B \downarrow$") that $T$ does not decide (for any formal system $T$ that is consistent and can reason about programs, e.g. PA).
The proof above can be formalized in $T$ (for $T$ that is consistent and can reason about programs), and shows that $T \vdash ($"$T$ is consistent" $\implies \sf B\uparrow)$.
But we just proved that $T \not\vdash \sf B\uparrow$! So (for $T$ that is consistent and can reason about programs), this means that $T \not\vdash$ "$T$ is consistent"!
Congrats! We've just proved the Gödel 2nd incompleteness theorem!
Finally, we return to the truth of whether or not $\sf B \downarrow$. Well, suppose that $\sf B \downarrow$. Analyzing the code, $\sf B\downarrow\iff$ we enter the 2nd "if" statement, and so there is some string $x$ that Verifier confirms is a $T$-proof that $B \uparrow$. If we $\color{red}{\textbf{assume}}$ that $T$ is "sound for program halting" (as explained by user21820 above), then we get a contradiction.
So (for $T$ that can reason about programs), we conclude that $T \vdash ($"$T$ is sound for program halting" $\implies \sf B\uparrow)$.
But remember we just proved (for $T$ that is consistent and can reason about programs) that $T \not\vdash \sf B\uparrow$! So (for $T$ that is consistent and can reason about programs), this means that $T \not\vdash$ "$T$ is sound for program halting"!
In conclusion, for say $T$ is PA (which can reason about programs --- by the Madhavan link I shared above; and which most of us assume is consistent and is sound for program halting), $$\sf B \uparrow$$ is an example of a true but PA-undecidable statement.
And we got all this, just by thinking about variations on a theme of barbers.
