Finiteness in infinite-valued Łukasiewicz logic

In this paper we deepen Mundici's analysis on reducibility of the decision problem from infinite-valued Łukasiewicz logic ℒ∞ to a suitable m-valued Łukasiewicz logic ℒm, where m only depends on the length of the formulas to be proved. Using geometrical arguments we find a better upper bound for the least integer m such that a formula is valid in ℒ∞ if and only if it is also valid in ℒm. We also reduce the notion of logical consequence in ℒ∞ to the same notion in a suitable finite set of finite-valued Łukasiewicz logics. Finally, we define an analytic and internal sequent calculus for infinite-valued Łukasiewicz logic.