FINITE AXIOMATIZATION OF

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

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).