On countermodels in basic logic

In [3] the tautology problem for Hájek's Basic Logic BL is proved to be co-NP-complete by showing that if a formula φ is not a tautology of BL then there exists an integer m > 0, polynomially bounded by the length of φ, such that φ fails to be a tautology in the infinite-valued logic mŁ corresponding to the ordinal sum of m copies of the Łukasiewicz t-norm. In this paper we state that if φ is not a tautology of BL then it already fails to be a tautology of a finite set of finite-valued logics, defined by taking the ordinal sum of m copies of k-valued Łukasiewicz logics, for effectively determined integers m, k > 0 only depending on polynomial-time computable features of φ. This result allows the definition of a calculus for mŁ along the lines of [1], [2], while the analysis of the features of functions associated with formulas of mŁ constitutes a step toward the characterization of finitely generated free BL-algebras as algebras of [0, 1]-valued functions.