Given its relevance for Open-source game theory, Dr. Andrew Critch asks the following about provability logic:
We conjecture that Löb’s Theorem can be proven without the use of the modal fixed point $\Psi$ ↔ ($\square \Psi$ → $C$), by constructing an entire proof that refers to itself, according to the following intuitive template:
- This proof is a proof of $C$.
- Therefore $\square C$.
- By assumption, $\square C \rightarrow C$.
- Therefore, by (2) and (3), $C$.
Is such a proof possible? If not, why not?
Where of course $\square$ is interpreted as the provability predicate. Thinking in PA, the idea would be to construct an object (a natural number) which encodes this self-referential proof. Some of the machinery in Boolos' The logic of provability is probably useful (especially the diagonal lemma).
My thoughts thus far:
Say $p(x, n)$ is the one-variable arithmetical formula encoding "$n$ is the Gödel number of a proof (in PA) of the sentence encoded by $x$". So that $\square C \equiv \exists n p(C, n)$.
Our object needs to somehow prove (1). So our object will look something like $$ n = \langle n_1, \ldots, n_k, \lceil p(C, n) \rceil, \lceil \exists n p(C, n) \rceil, \lceil \exists n p(C, n) \rightarrow C \rceil, \lceil C \rceil\rangle $$
The issue is the first $n_1, \ldots, n_k$ depend of course on the structure of $n$. We could specify them through a partial function $s(\lceil p(C, n) \rceil)$ which outputs the shortest proof of $\lceil p(C, n) \rceil$. But of course, we'd need to assume this value exists, and so already assume Löb is proved.
There must be some clever way of constructing the object which doesn't lead to regress. I've also tried using the diagonal lemma by specifying a property $P(G)$ which says something like "$G=\lceil p(C, n) \rceil$ and $n$ is the quine of itself with steps (2)-(4) added at the end" (that is, constructing a property defining the object). But the only way I've found to derive the existence of the object from the diagonal lemma is again by supposing we've proved Löb.
