×

Kripke semantics, undecidability and standard completeness for Esteva and Godo’s logic MTL\(\forall\). (English) Zbl 1013.03021

The logic MTL\(\forall\) is the predicate version of the monoidal t-norm based logic MTL introduced by F. Esteva and 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\).

MSC:

03B52 Fuzzy logic; logic of vagueness
03B50 Many-valued logic
03G25 Other algebras related to logic

Citations:

Zbl 0994.03017
PDFBibTeX XMLCite
Full Text: DOI