Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic (Q2212726)

On the basis of the calculus \(\mbox{G}Ł\forall\) of \textit{M. Baaz} and \textit{G. Metcalfe} in [J. Log. Comput. 20, No. 1, 35--54 (2010; Zbl 1188.03014); \textit{G. Metcalfe} et al., Proof theory for fuzzy logics. Dordrecht: Springer (2009; Zbl 1168.03002)] and tableau calculi by the author in [Algebra Logic 55, No. 2, 103--127 (2016; Zbl 1386.03025)], the author introduced in [Sib. Adv. Math. 28, No. 2, 79--100 (2018; Zbl 1413.03003] the analytic hypersequent calculi \(\mbox{G}^{1}Ł\forall\) and \(\mbox{G}^{2}Ł\forall\) for the first-order rational Pavelka logic \(\mbox{RPL}\forall\) and hence for the first-order infinite-valued Łukasiewicz logic \(Ł\forall\). The calculi \(\mbox{G}^{1}Ł\forall\) and \(\mbox{G}^{2}Ł\forall\) do not have structural rules; the latter is a noncumulative variant of the former, which is cumulative, i.e., preserves the conclusion of each inference rule in its premises. Any \(\mbox{G}Ł\forall\)- or \(\mbox{G}^{2}Ł\forall\)-provable sentence is provable in \(\mbox{G}^{1}Ł\forall\); any prenex \(\mbox{RP}\forall\)-sentence is \(\mbox{G}^{1}Ł\forall\) -provable iff it is \(\mbox{G}^{2}Ł\forall\)-provable; and any prenex \(Ł\forall\)-sentence is provable or unprovable in \(\mbox{G}Ł\forall\), \(\mbox{G}^{1}Ł\forall\) and \(\mbox{G}^{2}Ł\forall\) simultaneously. Also in [the author, 2018, loc. cit.], a family of proof search algorihms is described. Given a prenex \(\mbox{G}^2Ł\forall\)-provable sentence, such an algorithm constructs some proof for it in a tableau modification of the calculus \(\mbox{G}^{2}Ł\forall\). However this only works well for prenex sentences. A defect of \(\mbox{G}^{2}Ł\forall\) causes repeating designations of multisets of formulas in each premise of two quantifier rules. This causes repeated decomposition of the same formulas from the multisets during bottom-up proof search, and prevents establishing desirable proof-theoretic properties for the calculus \(\mbox{G}^{2}Ł\forall\). The present paper introduces an analytic hypersequent calculus \(\mbox{G}^{3}Ł\forall\) for the first-order infinite-valued Łukasiewicz logic \(Ł\forall\) and for the logic \(\mbox{RPL}\forall\). There are no structural rules in the calculus, and designations of multisets of formulas are not repeated in any premise of its rules. The calculus \(\mbox{G}^{3}Ł\forall\) proves any sentence that is provable in at least one of the previously known analytic calculi for \(Ł\forall\) or \(\mbox{RPL}\forall\), including Baaz and Metcalfe's [loc. cit.] hypersequent calculus \(\mbox{G}Ł\forall\) for \(Ł\forall\). Proof-theoretic properties of \(\mbox{G}^{3}Ł\forall\) are considered and foundations for proof search algorithms are given. A proof of the completeness of the \(\mbox{G}Ł\forall\)-based infinitary calculus for prenex \(Ł\forall\)-sentences is given. The completeness of a \(\mbox{G}^{3}Ł\forall\)-based infinitary calculus for prenex \(\mbox{RPL}\forall\)-sentences is established.