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

Didier Galmiche; Brandon Hornbeck; Daniel Méry

doi:10.18778/0138-0680.2026.11

Authors

Didier Galmiche Université de Lorraine, CNRS, LORIA Author https://orcid.org/0000-0002-9968-5323
Brandon Hornbeck Université de Lorraine, CNRS, LORIA Author
Daniel Méry Université de Lorraine, CNRS, LORIA Author https://orcid.org/0000-0002-1886-2106

DOI:

https://doi.org/10.18778/0138-0680.2026.11

Keywords:

non-Fregean sentential logic, sequent calculi, labeled calculi, nested sequents, proof translations

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.

References

S. Bloom, R. Suszko, Investigations into the Sentential Calculus with Identity, Notre Dame Journal of Formal Logic, vol. 13(3) (1972), pp. 289–308, DOI: https://doi.org/10.1305/ndjfl/1093890617.

S. Chlebowski, Sequent Calculi for SCI, Studia Logica, vol. 106(3) (2018), pp. 541–563, DOI: https://doi.org/10.1007/s11225-017-9754-8.

S. Chlebowski, Hyperintensionality, Identity and Excluded Middle, Logic and Logical Philosophy, (2025), pp. 1–24, DOI: https://doi.org/10.12775/LLP.2025.025.

S. Chlebowski, D. Leszczyńska-Jasion, An Investigation into Intuitionistic Logic with Identity, Bulletin of the Section of Logic, vol. 48(4) (2019), pp. 259–283, DOI: https://doi.org/10.18778/0138-0680.48.4.02.

M. Fitting, Nested Sequents for Intuitionistic Logics, Notre Dame Journal of Formal Logic, vol. 55(1) (2014), pp. 41–61, DOI: https://doi.org/10.1215/00294527-2377869.

D. Galmiche, M. Gawek, D. Méry, Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity, [in:] FSCD 2021, vol. 184 of LIPIcs (2021), pp. 13:1–13:21, DOI: https://doi.org/10.4230/LIPIcs.FSCD.2021.13.

D. Galmiche, D. Méry, Connection-based Proof Search in Intuitionistic Logic from Transitive Closure of Constraints, [in:] Proceedings of the International Workshop on Automated Deduction: Decidability, Complexity, Tractability (ADDCT 2007), Bremen, Germany (2007), available via HAL: hal-00580308.

J. Golińska-Pilarek, Rasiowa–Sikorski proof system for the non-Fregean sentential logic, Journal of Applied Non-Classical Logics, vol. 17(4) (2007), pp. 511–519, DOI: https://doi.org/10.3166/jancl.17.511-519.

J. Golińska-Pilarek, T. Huuskonen, M. Zawidzki, Tableau-based decision procedure for non-Fregean logic of sentential identity, [in:] CADE 28 (LNAI 12699) (2021), pp. 41–57, DOI: https://doi.org/10.1007/978-3-030-79876-5_3.

P. Łukowski, Intuitionistic sentential calculus with identity, Bulletin of the Section of Logic, vol. 19(3) (1990), pp. 92–99.

T. S. Lyon, On the correspondence between nested calculi and semantic systems for intuitionistic logics, Journal of Logic and Computation, vol. 31(1) (2021), pp. 213–265, DOI: https://doi.org/10.1093/logcom/exaa057.

A. Michaels, A uniform proof procedure for SCI tautologies, Studia Logica, vol. 33(3) (1974), pp. 299–310, DOI: https://doi.org/10.1007/BF02120864.

S. Negri, J. von Plato, Structural Proof Theory, Cambridge University Press (2001), DOI: https://doi.org/10.1017/CBO9780511527340.

E. Orłowska, J. Golińska-Pilarek, Dual Tableaux: Foundations, Methodology, Case Studies, vol. 33 of Trends in Logic, Springer (2011), DOI: https://doi.org/10.1007/978-94-007-0005-5.

E. Pimentel, R. Ramanayake, B. Lellmann, Sequentialising Nested Systems, [in:] Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019), vol. 11714 of LNCS, Springer (2019), pp. 147–165, DOI: https://doi.org/10.1007/978-3-030-29026-9_9.

L. Pinto, T. Uustalu, Relating Sequent Calculi for Bi-intuitionistic Propositional Logic, [in:] CL&C 2010, vol. 47 of EPTCS (2010), pp. 57–72, DOI: https://doi.org/10.4204/EPTCS.47.6.

S. Schmitt, C. Kreitz, On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs, [in:] Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX’95), vol. 918 of LNCS, Springer (1995), pp. 106–121, DOI: https://doi.org/10.1007/3-540-59338-1_31.

A. Tomczyk, D. Leszczyńska-Jasion, Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus, [in:] Proceedings of the 10th International Conference on Non-Classical Logics, Theory and Applications (NCL 2022), vol. 358 of EPTCS (2022), pp. 136–149, DOI: https://doi.org/10.4204/EPTCS.358.10.

A. Wasilewska, A sequence formalization for SCI, Studia Logica, vol. 35(3) (1976), pp. 213–217, DOI: https://doi.org/10.1007/BF02120674.

A. Wasilewska, DFC-algorithms for Suszko logic and one-to-one Gentzen type formalizations, Studia Logica, vol. 43(4) (1984), pp. 395–404, DOI: https://doi.org/10.1007/BF00370327.