Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic
Alexander Sergeyevich Gerasimov · Sibirskie Elektronnye Matematicheskie Izvestiya · 2020
We present an analytic hypersequent calculus G 3 L∀ for first-order infinite-valued Lukasiewicz logic L∀ and for an extension of it, first-order rational Pavelka logic RPL∀; the calculus is intended for bottom-up proof search.In G 3 L∀, there are no structural rules, all the rules are invertible, and designations of multisets of formulas are not repeated in any premise of the rules.The calculus G 3 L∀ proves any sentence that is provable in at least one of the previously known analytic calculi for L∀ or RPL∀, including Baaz and Metcalfe's hypersequent calculus G L∀ for L∀.We study proof-theoretic properties of G 3 L∀ and thereby provide foundations for proof search algorithms.We also give the first correct proof of the completeness of the G L∀-based infinitary calculus for prenex L∀-sentences, and establish the completeness of a G 3 L∀-based infinitary calculus for prenex RPL∀-sentences.