Finiteness in infinite-valued Łukasiewicz logic (Q1971778)

This paper strengthens 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\) only depends on the length of the formulas to be proved. Using geometrical arguments the authors obtain a better upper bound for the least integer \(m\) such that a formula is valid in \({\mathcal L}_\infty\). Furthermore the notion of logical consequence in \({\mathcal L}_\infty\) is reduced to the same notion in a suitable finite set of finite-valued Łukasiewicz logics. Finally, an analytic and internal sequent calculus for infinite-valued Łukasiewicz logic is defined.