Translating Labels to Hypersequents for Intermediate Logics with Geometric Kripke Semantics
Logic
2013-10-30 v3 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.1102.0240,
title = {Translating Labels to Hypersequents for Intermediate Logics with Geometric Kripke Semantics},
author = {Robert Rothenberg},
journal= {arXiv preprint arXiv:1102.0240},
year = {2013}
}
Comments
19 pages, 5 figures, 1 table, longer versions of proofs from conference paper and journal submission