Proof Translations between Label-free and Labeled Sequent Calculi in ISCI

Abstract

In this paper we consider the Intuitionistic Sentential Calculus with Identity (ISCI). We study two main families of sequent calculi. The first one, called G3ISCI, is based on a label-free multi-succedent sequent calculus that is sound and complete w.r.t. Kripke models and the second, called L3ISCI, is based on a multi-succedent labeled sequent calculus that is sound and complete w.r.t. Beth models. Our goal is to investigate how the calculi, that capture distinct semantics of the logic, relate to each other through proof translations. Proof translations from G3ISCI to L3ISCI provide new results about the soundness and (cut-free) completeness of G3ISCI w.r.t. Beth models. Proof translations from L3ISCI to G3ISCI are more difficult and require the definition of new calculi for ISCIthat provide intermediate steps in the translation process.