Skip to main content
2 of 3
edited tags
Glubs
  • 109
  • 4

Difference between provability and the existence of a proof?

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

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

Glubs
  • 109
  • 4