Skip to main content
MathOverflow

Return to Question

Became Hot Network Question
added 281 characters in body
Source Link
Glubs
Glubs
  • 109
  • 4

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.

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.

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.

edited tags
Link
Glubs
Glubs
  • 109
  • 4
Source Link
Glubs
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.