Paper detail

Trakhtenbrot theorem and first-order axiomatic extensions of MTL

In 1950, B.A. Trakhtenbrot showed that the set of first-order tautologies associated to finite models is not recursively enumerable. In 1999, P. Hájek generalized this result to the first-order versions of Łukasiewicz, Gödel and Product logics. In this paper we extend the analysis to the first-order axiomatic extensions of MTL. Our main result is the following. Let L be an axiomatic extension L of MTL s.t. TAUT$_\text{L}$ is decidable, and whose corresponding variety is generated by a chain: for every generic L-chain $\mathcal{A}$ the set fTAUT$^\mathcal{A}_{\forall}$ (the set of first-order tautologies associated to the finite $\mathcal{A}$-models) is $Π_1$. Moreover, if in addition L is an extension of BL or an extension of SMTL or an extension of WNM, then for every generic L-chain $\mathcal{A}$ the set fTAUT$^\mathcal{A}_{\forall}$ is $Π_1$-complete. More in general, for every axiomatic extension L of MTL s.t. TAUT$_\text{L}$ is decidable there is no L-chain $\mathcal{A}$ such that L$\forall$ is complete w.r.t. the class of finite $\mathcal{A}$-models. We have negative results also if we expand the language with the $Δ$ operator.