Deprenexification in analytic calculi for first-order rational Pavelka logic

We consider several finitary analytic hypersequent calculi for first-order infinite-valued Łukasiewicz logic Ł$\forall$ and for its expansion, first-order rational Pavelka logic $\mathrm{RPL}\forall$, including Baaz and Metcalfe's calculus $\mathrm{G}Ł\forall$ for Ł$\forall$. 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 $\mathcal{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 $\mathcal{H}$ by replacing the occurrence by $F$. Using this method, we establish the completeness of infinitary analytic calculi for Ł$\forall$ and $\mathrm{RPL}\forall$ that are based on the finitary calculi mentioned above. In particular, we give the first correct proof of the completeness of the $\mathrm{G}Ł\forall$-based infinitary analytic calculus for Ł$\forall$. Bibliography: 16 titles.