Kripke semantics, undecidability and standard completeness for Esteva and Godo's logic MTL\(\forall\) (Q1612691)

The logic MTL\(\forall\) is the predicate version of the monoidal t-norm based logic MTL introduced by \textit{F. Esteva} and \textit{L. Godo} [Fuzzy Sets Syst. 124, 271-288 (2001; Zbl 0994.03017)]. The axioms of MTL\(\forall\) are those of the predicate version of the Full Lambek Calculus FL\(_{\text{ew}}\) (i.e. FL plus exchange and weakening) plus \((A \rightarrow B) \vee (B \rightarrow A)\) and \(\forall x(A \vee B) \rightarrow (A \vee \forall x B)\) (\(x\) not free in \(A\)) in a Hilbert-style axiomatization with modus ponens and generalization. Basically, Kripke structures for MTL are precisely the structures for FL\(_{\text{ew}}\) which are linearly ordered. In the case of MTL\(\forall\), not only the corresponding models are linearly ordered, but the domains are constant, i.e. they do not depend on the node of the model. The first result of the present paper is a proof of completeness of MTL\(\forall\) with respect to this Kripke semantics. Then two applications of the Kripke completeness are considered: the undecidability and the standard completeness of MTL\(\forall\).