An incomplete system of modal logic (Q1073780)

The authors present a new system of modal propositional logic, called GH, that is ''incomplete in the following sense: there is a sentence that is not a theorem of GH even though it is valid in every frame in which all theorems of GH are valid''. This result is discussed with regard to the interpretation of '\(\square '\) as provability. The characteristic axiom of GH may then be read as saying that the sentences which are provably ''equivalent to their own provability are in fact provable''. It is thus a formalized answer to \textit{L. Henkin}'s question in ''A problem concerning provability'' [J. Symb. Logic 17, 160 (1952)], and it is closely related to Löb's theorem.