Deprenexification in analytic calculi for first-order rational Pavelka logic

We consider several finitary analytic hypersequent calculi for first-order infinite-valued Łukasiewicz logic Ł∀ and for its expansion, first-order rational Pavelka logic RPL∀, including Baaz and Metcalfe's calculus GŁ∀ for Ł∀. In these calculi the cut rule is not admissible and, in general, a formula and its (purely syntactically defined) prenex form are not equiprovable. However, we develop the method of deprenexification that allows us to perform the following transformation: a formal proof of a hypersequent H in which an occurrence of a prenex form of a formula F is distinguished can be transformed algorithmically into a formal proof of the hypersequent obtained from H by replacing the occurrence by F. Using this method, we establish the completeness of infinitary analytic calculi for Ł∀ and RPL∀ that are based on the finitary calculi mentioned above. In particular, we give the first correct proof of the completeness of the GŁ∀-based infinitary analytic calculus for Ł∀. Bibliography: 16 titles.