A repetition-free hypersequent calculus for first-order rational Pavelka logic

TL;DR

This paper introduces a new hypersequent calculus for first-order rational Pavelka logic that avoids structural rules and repetitions, facilitating more efficient proof search algorithms.

Contribution

The paper presents a repetition-free hypersequent calculus for first-order rational Pavelka logic, enhancing proof search capabilities and theoretical understanding.

Findings

The calculus proves all theorems of existing hypersequent calculi.

It has no structural rules and all rules are invertible.

Supports foundation for proof search algorithms.

Abstract

We present a hypersequent calculus $\text{G}^3\text{\L}\forall$ for first-order infinite-valued {\L}ukasiewicz logic and for an extension of it, first-order rational Pavelka logic; the calculus is intended for bottom-up proof search. In $\text{G}^3\text{\L}\forall$, 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 $\text{G}^3\text{\L}\forall$ proves any sentence that is provable in at least one of the previously known hypersequent calculi for the given logics. We study proof-theoretic properties of $\text{G}^3\text{\L}\forall$ and thereby provide foundations for proof search algorithms.