Unified Sequent Calculi and Natural Deduction Systems for Until-free Linear-time Temporal Logics

Norihiro Kamide; Sara Negri

doi:10.18778/0138-0680.2025.09

Authors

Norihiro Kamide Nagoya City University, School of Data Science https://orcid.org/0000-0001-7736-8055
Sara Negri University of Genoa, Department of Mathematics https://orcid.org/0000-0003-3958-6312

DOI:

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

Keywords:

linear-time temporal logic, intuitionistic linear-time temporal logic, sequent calculus, natural deduction, cut-elimination theorem, normalization theorem

Abstract

A unified Gentzen-style proof-theoretic framework for until-free propositional linear-time temporal logic and its intuitionistic variant is introduced. The framework unifies Gentzen-style single-succedent sequent calculi and natural deduction systems for both the classical and intuitionistic versions of these temporal logics. Theorems establishing the equivalence between the proposed sequent calculi and natural deduction systems are proved. Furthermore, the cut-elimination theorems for the proposed sequent calculi and the normalization theorems for the proposed natural deduction systems are established.

References

A. Abuin, A. Bolotov, M. Hermo, P. Lucio, Tableaux and sequent calculi for CTL and ECTL: Satisfiability test with certifying proofs and models, Journal of Logical and Algebraic Methods in Programming 130, 100828, (2023), DOI: https://doi.org/10.1016/J.JLAMP.2022.100828
Google Scholar DOI: https://doi.org/10.1016/j.jlamp.2022.100828

A. Almukdad, D. Nelson, Constructible falsity and inexact predicates, Journal of Symbolic Logic, vol. 49(1) (1984), pp. 231–233, DOI: https://doi.org/10.2307/2274105
Google Scholar DOI: https://doi.org/10.2307/2274105

S. Baratella, A. Masini, A proof-theoretic investigation of a logic of positions, Annals of Pure and Applied Logic, vol. 123 (2003), pp. 135–162, DOI: https://doi.org/10.1016/S0168-0072(03)00021-6
Google Scholar DOI: https://doi.org/10.1016/S0168-0072(03)00021-6

S. Baratella, A. Masini, An approach to infinitary temporal proof theory, Archive for Mathematical Logic, vol. 43(8) (2004), pp. 965–990, DOI: https://doi.org/10.1007/S00153-004-0237-Z
Google Scholar DOI: https://doi.org/10.1007/s00153-004-0237-z

Z.-E.-A. Benaissa, E. Moggi, W. Taha, T. Sheard, Logical modalities and multi-stage programming, [in:] Proceedings of Workshop on Intuitionistic Modal Logics and Applications (IMLA’99) (1999), 15 pp.
Google Scholar

A. Bolotov, A. Basukoski, O. M. Grigoriev, V. Shangin, Natural deduction calculus for linear-time temporal logic, [in:] Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA 2006), vol. 4160 of Lecture Notes in Computer Science (2006), pp. 56–68, DOI: https://doi.org/10.1007/11853886_7
Google Scholar DOI: https://doi.org/10.1007/11853886_7

A. Bolotov, V. Shangin, Natural deduction system in paraconsistent setting: Proof search for PCont, Journal of Intelligent Systems, vol. 21(1) (2012), pp. 1–24, DOI: https://doi.org/10.1515/JISYS-2011-0021
Google Scholar DOI: https://doi.org/10.1515/jisys-2011-0021

B. Boretti, S. Negri, Decidability for Priorean linear time using a fixed-point labelled calculus, [in:] Proceedings of the 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), vol. 5607 of Lecture Notes in Computer Science (2009), pp. 108–122, DOI: https://doi.org/10.1007/978-3-642-02716-1_9
Google Scholar DOI: https://doi.org/10.1007/978-3-642-02716-1_9

B. Boretti, S. Negri, On the finitization of Priorean linear time, [in:] M. D’Agostino, G. Giorello, F. Laudisa, T. Pievani, C. Sinigaglia (eds.), New Essays in Logic and Philosophy of Science, College Publications, London (2010), pp. 67–79.
Google Scholar

K. Brünnler, M. Lange, Cut-free sequent systems for temporal logic, Journal of Logical and Algebraic Methods in Programming, vol. 76(2) (2008), pp. 216–225, DOI: https://doi.org/10.1016/J.JLAP.2008.02.004
Google Scholar DOI: https://doi.org/10.1016/j.jlap.2008.02.004

S. Cerrito, V. Goranko, S. Paillocher, Partial model checking and partial model synthesis in LTL using a Tableau-based approach, [in:] Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction (FSCD) (2023), pp. 23:1–23:21, DOI: https://doi.org/10.4230/LIPICS.FSCD.2023.23
Google Scholar

R. Davies, A Temporal-Logic Approach to Binding-Time Analysis, [in:] Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society (1996), pp. 184–195, DOI: https://doi.org/10.1109/LICS.1996.561317
Google Scholar DOI: https://doi.org/10.1109/LICS.1996.561317

R. Davies, F. Pfenning, A modal analysis of staged computation, Journal of the ACM, vol. 48(3) (2001), pp. 555–604, DOI: https://doi.org/10.1145/382780.382785
Google Scholar DOI: https://doi.org/10.1145/382780.382785

E. A. Emerson, Temporal and modal logic, Elsevier and MIT Press (1990), pp. 995–1072, DOI: https://doi.org/10.1016/B978-0-444-88074-1.50021-4
Google Scholar DOI: https://doi.org/10.1016/B978-0-444-88074-1.50021-4

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, F. Orejas, A cut-free and invariant-free sequent calculus for PLTL, vol. 4646 of Lecture Notes in Computer Science, Springer (2007), pp. 481–495, DOI: https://doi.org/10.1007/978-3-540-74915-8_36
Google Scholar DOI: https://doi.org/10.1007/978-3-540-74915-8_36

Y. Gurevich, Intuitionistic logic with strong negation, Studia Logica, vol. 36 (1977), pp. 49–59.
Google Scholar DOI: https://doi.org/10.1007/BF02121114

S. Huang, R. Cleaveland, A tableau construction for finite linear-time temporal logic, Journal of Logical and Algebraic Methods in Programing, vol. 125 (2022), p. 100743, DOI: https://doi.org/10.1016/J.JLAMP.2021.100743
Google Scholar DOI: https://doi.org/10.1016/j.jlamp.2021.100743

N. Kamide, An equivalence between sequent calculi for linear-time temporal logic, Bulletin of the Section of Logic, vol. 35(4) (2006), pp. 187–194.
Google Scholar

N. Kamide, Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic, [in:] M. Fisher, F. Sadri, M. Thielscher (eds.), Computational Logic in Multi-Agent Systems, Springer Berlin Heidelberg, Berlin, Heidelberg (2009), pp. 57–76, DOI: https://doi.org/10.1007/978-3-642-02734-5_5
Google Scholar DOI: https://doi.org/10.1007/978-3-642-02734-5_5

N. Kamide, Notes on an extension of Davies’ logic for binding-time analysis, Far East Journal of Applied Mathematics, vol. 44(1) (2010), pp. 37–57.
Google Scholar

N. Kamide, Bounded linear-time temporal logic: A proof-theoretic investigation, Annals of Pure and Applied Logic, vol. 163(4) (2012), pp. 439–466, DOI: https://doi.org/10.1016/J.APAL.2011.12.002
Google Scholar DOI: https://doi.org/10.1016/j.apal.2011.12.002

N. Kamide, Temporal Gödel-Gentzen and Girard translations, Mathematical Logic Quarterly, vol. 59(1–2) (2013), pp. 66–83, DOI: https://doi.org/10.1002/MALQ.201100083
Google Scholar DOI: https://doi.org/10.1002/malq.201100083

N. Kamide, Embedding theorems for LTL and its variants, Mathematical Structures in Computer Science, vol. 25(1) (2015), pp. 83–134, DOI: https://doi.org/10.1017/S0960129514000048
Google Scholar DOI: https://doi.org/10.1017/S0960129514000048

N. Kamide, Interpolation theorems for some variants of LTL, Reports on Mathematical Logic, vol. 50 (2015), pp. 3–30, URL: https://rml.tcs.uj.edu.pl/rml-50/1-kamide.pdf
Google Scholar

N. Kamide, Relating first-order monadic omega-logic, propositional linear-time temporal logic, propositional generalized definitional reflection logic and propositional infinitary logic, Journal of Logic and Computation, vol. 27(7) (2017), pp. 2271–2301, DOI: https://doi.org/10.1093/LOGCOM/EXX006
Google Scholar DOI: https://doi.org/10.1093/logcom/exx006

N. Kamide, Natural deduction with explosion and excluded middle, [in:] Proceedings of the 53rd IEEE International Symposium on Multiple-valued Logic (ISMVL 2023) (2023), pp. 24–29, DOI: https://doi.org/10.1109/ISMVL57333.2023.00016
Google Scholar DOI: https://doi.org/10.1109/ISMVL57333.2023.00016

N. Kamide, Refutation-Aware Gentzen-Style Calculi for Propositional Until-Free Linear-Time Temporal Logic, Studia Logica, vol. 111(6) (2023), pp. 979–1014, DOI: https://doi.org/10.1007/S11225-023-10052-7
Google Scholar DOI: https://doi.org/10.1007/s11225-023-10052-7

N. Kamide, S. Negri, A unified Gentzen-style framework for until-free LTL, vol. 415 of Electronic Proceedings in Theoretical Computer Science (2024), pp. 165–179, DOI: https://doi.org/10.4204/EPTCS.415.16
Google Scholar DOI: https://doi.org/10.4204/EPTCS.415.16

N. Kamide, S. Negri, Proof theory for extended Belnap–Dunn and intuitionistic logics, Studia Logica, (2025), DOI: https://doi.org/10.1007/s11225-025-10203-y online first.
Google Scholar DOI: https://doi.org/10.1007/s11225-025-10203-y

N. Kamide, S. Negri, Unified natural deduction for logics of strong negation, Notre Dame Journal of Formal Logic, vol. 66(4) (2025), pp. 543–580, DOI: https://doi.org/10.1215/00294527-2025-0016
Google Scholar DOI: https://doi.org/10.1215/00294527-2025-0016

N. Kamide, H. Wansing, Combining linear-time temporal logic with constructiveness and paraconsistency, Journal of Applied Logic, vol. 8(1) (2011), pp. 33–61, DOI: https://doi.org/10.1016/J.JAL.2009.06.001
Google Scholar DOI: https://doi.org/10.1016/j.jal.2009.06.001

N. Kamide, H. Wansing, A paraconsistent linear-time temporal logic, Fundamenta Informaticae, vol. 106(1) (2011), pp. 1–23, DOI: https://doi.org/10.3233/FI-2011-374
Google Scholar DOI: https://doi.org/10.3233/FI-2011-374

H. Kawai, Sequential calculus for a first order infinitary temporal logic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 33 (1987), pp. 423–432, DOI: https://doi.org/10.1002/MALQ.19870330506
Google Scholar DOI: https://doi.org/10.1002/malq.19870330506

I. Kim, K. Yi, C. Calcagno, A polymorphic modal type system for lisp-like multi-staged languages, [in:] J. G. Morrisett, S. L. P. Jones (eds.), Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM (2006), pp. 257–268, DOI: https://doi.org/10.1145/1111037.1111060
Google Scholar DOI: https://doi.org/10.1145/1111037.1111060

K. Kojima, A. Igarashi, On constructive linear-time temporal logic, [in:] Proceedings of Intuitionistic Modal Logics and Applications Workshop (IMLA’08) (2008), 12 pp.
Google Scholar

N. Kürbis, Y. Petrukhin, Normalisation for some quite interesting many-valued logics, Logic and Logical Philosophy, vol. 30(3) (2021), pp. 493–534.
Google Scholar DOI: https://doi.org/10.12775/LLP.2021.009

E. Moggi, W. Taha, Z.-E.-A. Benaissa, T. Sheard, An Idealized MetaML: Simpler, and More Expressive, [in:] S. D. Swierstra (ed.), Proceedings of the 8th European Symposium on Programming (ESOP’99), vol. 1576 of Lecture Notes in Computer Science, Springer (1999), pp. 193–207, DOI: https://doi.org/10.1007/3-540-49099-X_13
Google Scholar DOI: https://doi.org/10.1007/3-540-49099-X_13

A. Nanevski, Meta-programming with names and necessity, [in:] M. Wand, S. L. P. Jones (eds.), Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), ACM (2002), pp. 206–217, DOI: https://doi.org/10.1145/581478.581498
Google Scholar DOI: https://doi.org/10.1145/581478.581498

S. Negri, Geometric rules in infinitary logic, [in:] O. Arieli, A. Zamansky (eds.), Arnon Avron on Semantics and Proof Theory of Non-Classical Logics, Outstanding Contributions to Logic, Springer (2021), pp. 265–293
Google Scholar DOI: https://doi.org/10.1007/978-3-030-71258-7_12

S. Negri, J. von Plato, Sequent calculus in natural deduction style, Journal of Symbolic Logic 66 (4), (2001), pp. 1803–1816, DOI: https://doi.org/10.2307/2694976
Google Scholar DOI: https://doi.org/10.2307/2694976

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

D. Nelson, Constructible falsity, Journal of Symbolic Logic, vol. 14 (1949), pp. 16–26, DOI: https://doi.org/10.2307/2268973
Google Scholar DOI: https://doi.org/10.2307/2268973

B. Paech, Gentzen-Systems for propositional temporal logics, [in:] E. Börger, H. K. Büning, M. M. Richter (eds.), CSL ’88, Springer Berlin Heidelberg, Berlin, Heidelberg (1989), pp. 240–253, DOI: https://doi.org/10.1007/BFb0026305
Google Scholar DOI: https://doi.org/10.1007/BFb0026305

R. Pliuškevičius, Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus, [in:] J. Bārzdinš, D. Bjørner (eds.), Baltic Computer Science, Springer Berlin Heidelberg, Berlin, Heidelberg (1991), pp. 504–528, DOI: https://doi.org/10.1007/BFb0019366
Google Scholar DOI: https://doi.org/10.1007/BFb0019366

A. Pnueli, The temporal logic of programs (1977), pp. 46–57, DOI: https://doi.org/10.1109/SFCS.1977.32
Google Scholar DOI: https://doi.org/10.1109/SFCS.1977.32

D. Prawitz, Natural deduction: a proof-theoretical study (1965), DOI: https://doi.org/10.2307/2271676
Google Scholar DOI: https://doi.org/10.2307/2271676

G. Priest, Natural Deduction Systems for Logics in the FDE Family, [in:] H. Omori, H. Wansing (eds.), New Essays on Belnap-Dunn Logic, Springer International Publishing, Cham (2019), pp. 279–292, DOI: https://doi.org/10.1007/978-3-030-31136-0_16
Google Scholar DOI: https://doi.org/10.1007/978-3-030-31136-0_16

M. E. Szabo, Collected papers of Gerhard Gentzen, [in:] M. E. Szabo (ed.), Studies in Logic and the Foundations of Mathematics, North-Holland (1969), DOI: https://doi.org/10.2307/2272429 english translation.
Google Scholar DOI: https://doi.org/10.2307/2272429

M. E. Szabo, A sequent calculus for Kröger logic, [in:] A. Salwicki (ed.), Logics of Programs and Their Applications, Springer Berlin Heidelberg, Berlin, Heidelberg (1983), pp. 295–303, DOI: https://doi.org/10.1007/3-540-11981-7_21
Google Scholar DOI: https://doi.org/10.1007/3-540-11981-7_21

W. Taha, T. Sheard, Multi-Stage Programming with Explicit Annotations, [in:] J. P. Gallagher, C. Consel, A. M. Berman (eds.), Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’97), ACM (1997), pp. 203–217, DOI: https://doi.org/10.1145/258993.259019
Google Scholar DOI: https://doi.org/10.1145/258993.259019

L. Tranchini, Natural deduction for bi-intuitionistic logic, Journal of Applied Logic, vol. 25(Supplement) (2017), pp. S72–S96, DOI: https://doi.org/10.1016/J.JAL.2017.12.001
Google Scholar DOI: https://doi.org/10.1016/j.jal.2017.12.001

A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, vol. 45 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, (2000), DOI: https://doi.org/10.1017/CBO9781139168717
Google Scholar DOI: https://doi.org/10.1017/CBO9781139168717

J. von Plato, Proof theory of full classical propositional logic (1999), manuscript, 16 pp.
Google Scholar

J. von Plato, Elements of Logical Reasoning (2014), DOI: https://doi.org/10.1017/CBO9781139567862
Google Scholar DOI: https://doi.org/10.1017/CBO9781139567862

J. von Plato, Saved from the Cellar: Gerhard Gentzen’s Shorthand Notes on Logic & Foundations of Mathematics (2017), DOI: https://doi.org/10.1007/978-3-319-42120-9
Google Scholar DOI: https://doi.org/10.1007/978-3-319-42120-9

Y. Yuse, A. Igarashi, A modal type system for multi-level generating extensions with persistent code, [in:] A. Bossi, M. J. Maher (eds.), Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, ACM (2006), pp. 201–212, DOI: https://doi.org/10.1145/1140335.1140360
Google Scholar DOI: https://doi.org/10.1145/1140335.1140360