Proof theory for locally finite many-valued logics: semi-projective logics (Q385019)

As the authors explain, the aim of the article is to extend the methodology in [\textit{M. Baaz} and \textit{C. G. Fermüller}, Lect. Notes Comput. Sci. 1617, 36--50 (1999; Zbl 0931.03066)] to systematically construct analytic calculi for semi-projective logics -- a large family of (propositional) locally finite many-valued logics. Such calculi, defined in the framework of sequents of relations, are proof search oriented and can be used to settle the computational complexity of the formalized logics. As a case study they derive sequent calculi of relations for nilpotent minimum logic (see [\textit{F. Esteva} and \textit{L. Godo}, Fuzzy Sets Syst. 124, No. 3, 271--288 (2001; Zbl 0994.03017)]) and for a family of axiomatic extensions of Hájek's basic logic BL extended with the \(n\)-contraction axiom, (see [\textit{M. Bianchi} and \textit{F. Montagna}, Arch. Math. Logic 50, No. 3--4, 257--285 (2011; Zbl 1266.03041)]). The introduced calculi are used to prove that the decidability problem in these logics is Co-NP complete. The main results are in Sections 3 to 5. Section 3 is about semi-projective logics, and presents a general method to construct an analytic calculi, for them. It is shown, among the other things, that every semi-projective logic with finitely-many connectives and constants is locally finite, and that all semi-projective logics are decidable. These results are then applied in Section 4, to present an analytic calculi for NM and for a family of \(n\)-contractive axiomatic extensions of BL. Moreover, it is also shown that such calculi provide a Co-NP decision procedure for the validity problem of these logics. Finally, in Section 5 is discussed the problem of defining analytic calculi for first-order many-valued logics, and most of the results are negative.