Formulas of the propositional modal language with the unary modal operators
, etc. are considered as schemata of sentences of arithmetic (PA), where
is interpreted as (a formalization of) “
is PA- provable”,
is PA-equivalent to a
- sentence” and
is PA-equivalent to a Boolean combination of
-sentences”. We give an axiomatization and show decidability of the sets of the modal formulas which are schemata of: (1) PA-provable, (2) true arithmetical sentences.