Refutation calculi for lattice-based logics: from display to tableaux
For logicians working on proof theory, this extends refutation calculi to display calculi, a previously unexplored area.
This paper introduces refutation display calculi for basic LE-logics, proving soundness and completeness, and derives terminating tableaux calculi from them.
Refutation calculi are formal systems developed to derive the invalid formulas of a given logic. While the notion of refutation calculi has played a key role in the development of tableaux calculi, a refutation approach to display calculi has not yet been attempted. In this paper, we introduce refutation display calculi for basic LE-logics, i.e., those logics canonically associated with basic normal lattice expansions of any signature. In particular, we prove soundness and completeness via proof-analysis results on derivable sequents. Finally, we obtain terminating tableaux calculi from these refutation display calculi.