Proof Theory for Lax Logic

TL;DR

This paper develops a proof-theoretic framework for propositional Lax Logic, introducing a cut-free sequent calculus and demonstrating uniform interpolation through proof-based methods, offering a new perspective beyond model-based proofs.

Contribution

It presents the first proof-theoretic sequent calculus for Lax Logic and provides a direct proof of interpolation using this calculus, advancing the understanding of the logic's proof systems.

Findings

Established a cut-free, terminating sequent calculus for Lax Logic

Proved that Lax Logic has uniform interpolation using the calculus

Provided a simple, proof-based proof of interpolation for Lax Logic

Abstract

In this paper some proof theory for propositional Lax Logic is developed. A cut free terminating sequent calculus is introduced for the logic, and based on that calculus it is shown that the logic has uniform interpolation. Furthermore, a separate, simple proof of interpolation is provided that also uses the sequent calculus. From the literature it is known that Lax Logic has interpolation, but all known proofs use models rather than proof systems.