Skip to main content
added 877 characters in body
Source Link
Nik Weaver
  • 42.8k
  • 3
  • 112
  • 213

I think this question is clearly asking for provability logic. This is the basic modal logic K with the additional axiom

$$\square(\square A \to A) \to \square A.$$

"$\square A$" is interpreted as "$A$ is provable" (with reference to some fixed target formal system).

Edit: the specific question of being able to prove the second incompleteness theorem in provability logic (the answer is yes) has been discussed on philosophy.stackexchange and math.stackexchange.


Just to be clear, the above refers to provability within a specific formal system. The general semantic notion of provability, in the sense of "demonstrable with rational certainty", outside of any fixed formal system has been axiomatized in this book. That is a much more subtle notion, but it can be consistently axiomatized.

I think this question is clearly asking for provability logic. This is the basic modal logic K with the additional axiom

$$\square(\square A \to A) \to \square A.$$

"$\square A$" is interpreted as "$A$ is provable" (with reference to some fixed target formal system).

I think this question is clearly asking for provability logic. This is the basic modal logic K with the additional axiom

$$\square(\square A \to A) \to \square A.$$

"$\square A$" is interpreted as "$A$ is provable" (with reference to some fixed target formal system).

Edit: the specific question of being able to prove the second incompleteness theorem in provability logic (the answer is yes) has been discussed on philosophy.stackexchange and math.stackexchange.


Just to be clear, the above refers to provability within a specific formal system. The general semantic notion of provability, in the sense of "demonstrable with rational certainty", outside of any fixed formal system has been axiomatized in this book. That is a much more subtle notion, but it can be consistently axiomatized.

Source Link
Nik Weaver
  • 42.8k
  • 3
  • 112
  • 213

I think this question is clearly asking for provability logic. This is the basic modal logic K with the additional axiom

$$\square(\square A \to A) \to \square A.$$

"$\square A$" is interpreted as "$A$ is provable" (with reference to some fixed target formal system).