Trakhtenbrot theorem and first-order axiomatic extensions of MTL

preprint2014arXivOpen access

Abstract

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. TAUTL_\text{L} is decidable, and whose corresponding variety is generated by a chain: for every generic L-chain A\mathcal{A} the set fTAUT∀A^\mathcal{A}_{\forall} (the set of first-order tautologies associated to the finite A\mathcal{A}-models) is Π1Π_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 A\mathcal{A} the set fTAUT∀A^\mathcal{A}_{\forall} is Π1Π_1-complete. More in general, for every axiomatic extension L of MTL s.t. TAUTL_\text{L} is decidable there is no L-chain A\mathcal{A} such that L∀\forall is complete w.r.t. the class of finite A\mathcal{A}-models. We have negative results also if we expand the language with the ΔΔ operator.

Explore this paper’s authors, topics and related work.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Reviews 0

Write a reviewWrite

No reviews yet.

Discussion 0

Add a commentWrite

No comments yet.