Effectively constructible fixed points in Sacchetti's modal logics of provability (Q2134275)

As a weaker version of the provability modal logic GL Sacchetti introduced for each \(n<\omega\) a normal modal logic \(wGLn\) which is obtained by replacing the second-left box-operator in the Löb-axiom of (standard axiomatization of) GL by its \((n+1)\)-iteration. The family of \(wGLn\) \((n<\omega)\) constitutes a descending chain of sublogics of GL so that the modality formalizes the \(\sum_n\)-provability, where the completeness is established by Kurahashi with respect to the non-standard arithmetical provability. Sacchetti also proved several fixed-point properties of \(wGLn\) similarly to those of GL in a semantical method, where for GL their proofs have been given not only semantically by Smorynski, et. al., but also syntactically by Sambin. In this case the difference between the two proofs is essential in the sense that the latter provides an effective procedure of fixed point construction as well. So, Sacchetti asked if there is such a constructive one for \(wGLn\) as well. Answering to this question, in this paper, the authors establish the syntactic proof, which is carried out essentially by an induction on the modal depth of propositional variable occurrence in a given formula based on the equivalence provable in \(wGLn\) between \(n\)-modalized propositional variable and modalized falsity. It is also remarked that certain particular modal formulas enjoy simpler fixed-points as well.