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.



Difference between provability and the existence of a proof?
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.


