Labelled tableaux for interpretability logics

TL;DR

This paper introduces a labelled tableau proof system applicable to a broad class of interpretability logics, enhancing proof-theoretical understanding by establishing soundness and completeness for logics characterized by specific frame conditions.

Contribution

It presents a new labelled tableau system that is sound and complete for interpretability logics defined by universal Horn frame conditions.

Findings

System is sound and complete for the targeted interpretability logics.

Extends proof-theoretical tools for interpretability logics.

Provides a unified framework for a wide class of interpretability logics.

Abstract

In is paper we present a labelled tableau proof system that serves a wide class of interpretability logics. The system is proved sound and complete for any interpretability logic characterised by a frame condition given by a set of universal strict first order Horn sentences. As such, the current paper adds to a better proof-theoretical understanding of interpretability logics.