# Why isn't GL system of provability logic reflexive?

Formula $\square p \rightarrow p$ (axiom T; corresponding to reflexive modal frames) is interpreted as "if p is provable, then p", or more precisely: for all realizations (all substitutions for $p$), $PA \vdash Bew(\ulcorner p \urcorner) \rightarrow p$ (PA is system whose provability we discuss, i.e. some standard first-order axiomatization of Peano Arithmetic).

Now if we forget the fact that T combined with Gödel-Löb axiom produces a contradiction-proving disaster, what I'm wondering is what is intuitively wrong with T? Because to me it seems perfectly obvious that if we have a proof of $p$, then we also have $p$, since $p$ is just the last step of the mentioned proof. How can we have a proof (in PA) of something that doesn't hold (in PA)? Since proof is nothing more than coded array of sentences, we can simply follow its steps and get to $p$.

Even $\square \bot \rightarrow \bot$ seems ok: if we can prove $\bot$, then $\bot$ does hold in this system (it's not T's fault that we're dealing with inconsistent system).

I'm new to provability logic (just started reading The Logic of Provability) so I guess I'm overlooking something obvious. Thanks!

-
Axiom T, interpreted in provability logic, asserts that the logical system is sound. But what if $\Box$ isn't the "true" provability predicate? For example, suppose we have a non-standard model of PA. Then it is conceivable that there is a non-standard number that codes the proof of a contradiction... – Zhen Lin Jul 8 '12 at 8:34
What is "Löb-Geach axiom"? This very post is the first Google hit for "Löb-Geach" (and the only hit on the first page that actually contains "geach" and not "beach"). – Henning Makholm Jul 8 '12 at 11:38
Yes, sorry, Gödel-Löb (axiom GL) it is. – Luka Mikec Jul 8 '12 at 13:01

This is an area where it is very easy to get oneself confused from lack of precision. You write ${\it Bew}(\ulcorner p\urcorner)$ without specifying which axioms $p$ is to be proved from, and that makes an important difference.

Let's first consider $$T_0(p) \equiv {\it Bew}_{PA}(\ulcorner p \urcorner)\to p$$ There's nothing wrong with this; if we believe in Peano Arithmetic at all, it must be true in the standard model, and so in particular $PA+T_0$ is consistent. (In general I will tacitly assume that $PA$ is true and consistent).

On the other hand, individual instances of $T_0$ are not necessarily theorems of $PA$. Because of Gödel-Rosser's incompleteness theorem, there is a model of $PA$ in which ${\it Bew}_{PA}(\ulcorner \bot\urcorner)$ is true. But that means that in that model $T_0(\bot)$ is false -- so it cannot be a theorem.

In fact, Löb's theorem shows that $T_0(p)$ is a theorem of $PA$ if and only if $p$ itself is.

Since $T_0$ is consistent with $PA$ (and even true), we can choose to adopt it as an axiom. We may then consider $$T_1 \equiv {\it Bew}_{PA+T_0}(\ulcorner p\urcorner)\to p$$ The story of $T_1$ is then much the same as that of $T_0$: We can convince ourselves that it is consistent with $PA+T_0$, in fact true in the standard model, but not a theorem of $PA+T_0$. And we can then continue by induction to $$T_n \equiv {\it Bew}_{PA+T_0+T_1+\cdots+T_{n-1} }(\ulcorner p\urcorner) \to p$$ for any finite $n$.

However, bad things happen if we attemt to "go to the limit" and consider $$T_\infty(p) \equiv {\it Bew}_{PA+T_\infty}(\ulcorner p\urcorner)\to p$$ Note that instead of a limiting process we could have arrived at $T_\infty$ directly by being sloppy about the precise meaning of $\Box$ in the pithy formulation "take $\Box p \to p$ as an axiom".

First, it isn't immediately clear that $T_\infty$ is well-defined at all, but I think, without having checked the details, that one of the recursion theorems can produce a formula that meets the above specification. So let's put that objection aside.

It is a much more serious problem that $T_\infty$ directly implies that $PA+T_\infty$ is consistent! That means that $PA+T_\infty$ can prove its own consistency and (Gödel-Rosser again) this is an offense punishable by inconsistency. So $T_\infty$ is not consistent with $PA$.

If we unfold the construction in the proof of Gödel-Rosser, we would get a concrete $p_0$ such that $PA \vdash \neg T_\infty(p_0)$. But that is not very enligthening, so let's instead consider intuitively why our intuition that $T_n$ must be true doesn't work for $T_\infty$.

Suppose we have a proof of some sentence $p$ from $PA+T_\infty$; we wish to convince ourselves that then $p$ is indeed true. The proof is a certain finite sequence of formulas; we can check one by one that each of these formulas is true, given that all of the previous ones. Except, that is, if one of the formulas is an instance of $T_\infty$ and is justified by "that is an axiom". Since the truth of $T_\infty$ was what we were trying to argue for, we cannot just assume it at that point. And it won't work to attempt to justify it by induction either, because there is no guarantee that the proof the "inner" $T_\infty$ is applied to is shorter or simpler than the outer one. So we might find ourselves in an infinite ascent there.

In the first version of this answer I wrote $T_\omega$ instead of $T_\infty$, but arguably $T_\infty$ isn't really the limit of the $T_n$s. In fact, we can continue the $T_n$ sequence transfinitely to $$T_\omega \equiv {\it Bew}_{PA+T_0+T_1+\cdots+T_n+\cdots }(\ulcorner p\urcorner) \to p$$ and indeed $$T_\alpha \equiv {\it Bew}_{PA+\{T_\beta\mid\beta < \alpha\} }(\ulcorner p\urcorner) \to p$$ for as many ordinals as we can describe in $PA$ in the first place. Neither of these have the circularity problem that plague $T_\infty$.

-
Thank you for very detailed answer! Can you explain this part a bit more: "On the other hand, individual instances of $T_0$ are not necessarily theorems (...) so it cannot be a theorem"? How does incompleteness theorem imply that there must be a model in which ${\it Bew}(\ulcorner PA\vdash \bot\urcorner)$? How could such deviant model be built? Decoding and checking proofs seem to be trivial operations. – Luka Mikec Jul 8 '12 at 13:25
The incompleteness theorem tells us that if $PA$ is consistent, then $PA$ cannot prove ${\it Con}_{PA}$. One way to express ${\it Con}_{PA}$ is $PA \not\vdash \bot$. Because $PA$ cannot prove this, $PA \cup \{{\it Bew}_{PA}(\ulcorner \bot \urcorner)\}$ is a consistent theory (otherwise the contradiction would amount to an indirect proof of ${\it Con}_{PA}$ in $PA$ itself). By the completeness theorem, this consistent theory has a model. (The completeness theorem is not very constructive, so it is hard to exhibit this model explicitly -- but is has to be out there somewhere). – Henning Makholm Jul 8 '12 at 13:30
Nonstandard models of $PA$ contain elements that are "infinitely large" seen from the outside. Something that the nonstandard model thinks is a proof of $\bot$ would be one of those infinities, so the proof cannot actually be decoded and checked in finite time. (The nonstandard model itself thinks it can, but that is only because the model is deluded about what "finite" means). – Henning Makholm Jul 8 '12 at 13:37
Thanks! I think I get it now. – Luka Mikec Jul 8 '12 at 14:23