Translating Labels to Hypersequents for Intermediate Logics with Geometric Kripke Semantics

TL;DR

This paper develops a systematic method to translate geometric Kripke frame axioms and labelled sequents into hypersequent rules and proofs for intermediate logics, facilitating proof translation and analysis.

Contribution

It introduces a procedure for translating geometric Kripke axioms into hypersequent rules and labelled sequents into hypersequent proofs, expanding proof-theoretic tools for intermediate logics.

Findings

Translation preserves linear models, including G"odel-Dummett logic.

Hypersequent proofs can incorporate the linearity rule, akin to the communication rule.

The method enables proof translation between labelled and hypersequent systems.

Abstract

We give a procedure for translating geometric Kripke frame axioms into structural hypersequent rules for the corresponding intermediate logics in Int^*/Geo that admit weakening, contraction and in some cases, cut. We give a procedure for translating labelled sequents in the corresponding logic to hypersequents that share the same linear models (which correspond to G\"odel-Dummett logic). We prove that labelled proofs Int^*/Geo can be translated into hypersequent proofs that may use the linearity rule, which corresponds to the well-known communication rule for G\"odel-Dummett logic.