Kripke completeness, undecidability and standard completeness for Esteva and Godo's logic MTLforall

The present paper deals with the predicate version MTLV of the logic MTL by Esteva and Godo. We introduce a Kripke semantics for it, along the lines of Ono's Kripke semantics for the predicate version of FLew (cf. [O85]), and we prove a completeness theorem. Then we prove that every predicate logic between MTL∀ and classical predicate logic is undecidable. Finally, we prove that MTL∀ is complete with respect to the standard semantics, i.e., with respect to Kripke frames on the real interval [0, 1], or equivalently, with respect to MTL-algebras whose lattice reduct is [0, 1] with the usual order. © 2002 Kluwer Academic Publishers.