1-consistency and the diamond (Q1074577)

The modal propositional logic G is known to be complete for interpretation of \(\square A\) as the provability of A in the first order arithmetic PA. In a previous paper [Stud. Logica 39, 237-243 (1980; Zbl 0464.03049)], the author modified the proof of this fact to show that provability of A can be replaced by omega-derivability [by which he means provability of \(\forall nF(n)\to A\) with F(n) provable in PA for any number n]. Here the construction is modified to show that \(\square A\) can also be interpreted as 1-provability, i.e. omega-derivability for primitive recursive F. A similar completeness result for the logic \(G^*\) (when the provability of the arithmetic interpretation is replaced by its truth) is also obtained, as well as refinements concerning existence of uniform refuting substitutions for underivable propositional formulas.