Infinite-valued first-order Łukasiewicz logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form

The rational first-order Pavelka logic is an expansion of the infinite-valued first-order Łukasiewicz logic Ł$\forall$ by truth constants. For this logic, we introduce a cumulative hypersequent calculus G$^1$Ł$\forall$ and a noncumulative hypersequent calculus G$^2$Ł$\forall$ without structural inference rules. We compare these calculi with the Baaz–Metcalfe hypersequent calculus GŁ$\forall$ with structural rules. In particular, we show that every GŁ$\forall$-provable sentence is G$^1$Ł$\forall$-provable and a Ł$\forall$-sentence in the prenex form is GŁ$\forall$-provable if and only if it is G$^2$Ł$\forall$-provable. For a tableau version of the calculus G$^2$Ł$\forall$, we describe a family of proof search algorithms that allow us to construct a proof of each G$^2$Ł$\forall$-provable sentence in the prenex form.