Finite-valued reductions of infinite-valued logics (Q1407546)

In J. Logic Lang. Inf. 9, 5-29 (2000; Zbl 0951.03024), the first author and \textit{A. Ciabattoni} presented a strengthening of Mundici's analysis [\textit{D. Mundici}, Theor. Comput. Sci. 52, 145-153 (1987; Zbl 0639.03042)] on the reducibility of the decision problem in propositional infinite-valued Łukasiewicz logic \({\mathcal L}_\infty\) to the same problem in a suitable set of \(m\)-valued Łukasiewicz logics \({\mathcal L}_m\), where \(m\) depends only on the length of the formulas to be proved. The present paper extends these methods and results to Gödel logic and product logic, and to logics obtained by combining Gödel and Łukasiewicz connectives. The results related to Gödel logic are known [\textit{P. Hájek}, Metamathematics of fuzzy logic (1998; Zbl 0937.03030)], but the method applied here and the reduction of formulas of product logic to finite-valued logics are new. A calculus is defined for all these infinite-valued logics. It depends on the rules reducing the infinite-valued tautology problem to its finite-valued counterpart. Sequent calculi are provided that are based on the proof-theoretic machinery of the first author, \textit{A. Ciabattoni} and \textit{A. Di Nola} [J. Log. Comput. 10, 213-222 (2000; Zbl 0955.03031)]. To conclude, it is shown that the tautology problem for all considered infinite-valued logics is in co-NP. In the case of product logic the presented proof is alternative to the one given by \textit{M. Baaz}, \textit{P. Hájek}, \textit{J. Krajíček} and \textit{D. Svejda} [Stud. Log. 61, 35-47 (1998; Zbl 0962.03019)].