Difference between provability and the existence of a proof?

Question

In provability logic, $\square X \rightarrow X$ is not a theorem.

In my head[1] this reads as "if X is provable you don't necessarily have a proof of X".

This has lead to the question, what does provable even mean, if not there exists a proof of X? Is there an example of some proposition that is provable but does not have a proof?

Please help

edit: Maybe I didn't make myself clear, $X \rightarrow \square X$ is a theorem in provability logic. This means that $X \not\simeq \square X$. Which means that a proof of X is not equivalent to that proposition being provable, which is very strange to me.

^[1] I come from type theory so I tend to think constructively.

Answer 1

First note this isn't a constructive logic, so it's wrong to think of "$X$" as "there is a proof of $X$". (Even in constructive logic I find that dubious.)

Second note that if $X$ is provable then $Y \rightarrow X$ is provable for any $Y$. So it's not correct to say that $\square X \rightarrow X$ is not a theorem. The correct statement is that it's a theorem if and only if $X$ is a theorem (assuming your base logic is consistent). So any time you might want to use this implication, because the hypothesis holds, you can in fact use it.

A more interesting statement is that the universal $\forall X : \square X \rightarrow X$ is not a theorem. In other words, we can't prove that any time we prove any statement, that statement is true. This makes it more clear that the issue in question is trust. The formal system does not trust that necessarily every statement it can prove is true.

Another perspective on the statement consists of looking at nonstandard models. Every formal system will have nonstandard models that contain "natural numbers" that, from our perspective, are larger than all actual natural numbers. One of these numbers can encode a "proof" of $X$, from the perspective of the model that, in our world, is infinitely long, and therefore is not a real proof. This can happen even if $X$ is not true.

So in a nonstandard models, there can be statements that are provable in the sense that they have a proof encoded by a number understood by that model but don't have a proof in the sense of an actual finite string of symbols.

Answer 2

There is a subtle point to make between the verificationist notion of proof and the notion of proof captured by $\Box$ in GL Provability Logic.

In GL, $\Box p$ is interpreted to be $Bew(\ulcorner p \urcorner)$, which is an encoding in an arithmetic theory $\mathcal T$ of a proof of $p$ in $\mathcal T$.

Verificationist logics use a broader, slightly nebulous notion of proof, which is not limited to proofs in a theory that can be encoded by that theory. Some verificationists would say that a proof is anything that can be constructively demonstrated according to axioms and/or inference rules. In this way, a verificationist can speak about different orders of mathematical/logical language without having to talk about different provability predicates/operators.

This difference is elucidated by the hallmark result of provability logic, namely Löb’s Theorem: $\Box (\Box p \to p) \to \Box p$. This result amounts to the fact that arithmetic theories are incomplete, which implies that they cannot prove either consistency or soundness. Since $\Box (\Box p \to p)$ is an encoding of a proof of localized soundness w.r.t $p$, we can’t have soundness for the whole system be provable in the system since per Löb, $\Box \bot$ would then be a theorem. However, verificationist notions of proof don’t make reference to a specific proof system, but rather validate what holds for a prover that is capable of always using stronger theories. As such, some reasonable assumptions like “if $p$ is provably provable, then $p$ is provable,” are made. This is clearly a desirable result, especially for a propositional logic in which formulas are interpreted in terms of what a thinking agent can prove, as opposed to what can be encoded by a formal theory.

As a side-note, I prefer to say “$p$ is verified” as opposed to “$p$ is provable” in verificationist contexts.

Answer 3

The issue has indeed arisen in Gödel's incompleteness theorems, and the asymmetry between $P \to \square P$ and $\square P \to P$ is understood by the realization that, while provability is a metatheoretic concept, the internal provability captured by the operator $\square$ is indeed a more stringent concept. It is how the theory itself can perceived the notion of provability, as internalized e.g. by arithmetization of syntax via Gödel numbers. When one internalizes, the reach of what is provable changes.

$P \to \square P$ is a theorem with respect to the notion of external provability, which is the metatheoretic concept which exceeds the notion that can be described only within the theory itself. The fact that $\square P \to P$ is not always (externally) provable reflects the fact that in general the internal provability is a stronger notion than external provability, in the sense that it the set of statements $P$ for which $\square P$ holds is a proper quotient of the original theory where new statements become internally provable that are not externally provable (e.g., a consistent theory can be internally inconsistent).

What this phenomenon shows is that any method for internalizing the metatheoretic notion of provability within the theory itself is not going to capture the exact same notion, unless the original theory is itself inconsistent. This remarks the need to get out of the system to really understand the metatheoretic concepts about the system itself.