FINITE AXIOMATIZATION OF Grz × S 5 Grz× S5 bold upper G r z times bold upper S Baseline bold 5 AND GL × S 5 GL× S5 bold upper G upper L times bold upper S Baseline bold 5

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 GL × S5 bold upper G upper L times bold upper S Baseline bold 5 is product matching, and that Grz × S 5 Grz × S5 bold upper G r z times bold upper S Baseline bold 5 is axiomatized by adding to the commutator [ Grz , S 5 ] [Grz,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).