FINITE AXIOMATIZATION OF Grz × S 5 $\mathbf {Grz}\times \mathbf {S5}$ bold upper G r z times bold upper S Baseline bold 5 AND GL × S 5 $\mathbf {GL}\times \mathbf {S5}$ bold upper G upper L times bold upper S Baseline bold 5

Abstract We develop a selective filtration technique for the monadic Grzegorczyk and Gödel–Löb logics with the monadic Barcan formula, yielding that these logics have the finite model property. As a consequence, we obtain that GL × S 5 $\mathbf {GL} \times \mathbf {S5}$ bold upper G upper L times bold upper S Baseline bold 5 is product matching, and that Grz × S 5 $\mathbf {Grz} \times \mathbf {S5}$ bold upper G r z times bold upper S Baseline bold 5 is axiomatized by adding to the commutator [ Grz , S 5 ] $[\mathbf {Grz},\mathbf {S5}]$ left bracket bold upper G r z comma bold upper S Baseline bold 5 right bracket the Gödel translation of the monadic Casari formula. This settles the question of finite axiomatization for two of the product logics listed in [13, p. 137] . As another consequence, we obtain that the one-variable fragments of the predicate Grzegorczyk and Gödel–Löb logics with the Barcan formula are Kripke complete (which contrasts the incompleteness of the full predicate logics).