Finiteness in infinite-valued Lukasiewicz logic

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