Loop-type sequent calculi for temporal logic (Q2228437)

Loop-type sequent calculi were first considered in [\textit{P. Wolper}, Log. Anal., Nouv. Sér. 28, 119--136 (1985; Zbl 0585.03008)]. observing that some global constraints (\textit{loops}) must be detected on branches to identify a tree as a proof. This approach uses loops not only for closing failed proof trees as in standard cases but also for playing the role of axioms. The loop-type sequent calculi for \(\mathbf{BDI}\) (Beliefs, Desires, Intentions) logic based on \(\mathbf{CTL}\) were presened in [\textit{N. Naoyuki} et al., Electron. Notes Theor. Comput. Sci. 70, No. 5, 140--152 (2002; Zbl 1270.68286)]. Loop-type sequent calculi for temporal, mutual belief and dynamic logics were considered in [\textit{A. Pliuškevičienė}, Liet. Mat. Rink. 41, 413--420 (2001; Zbl 1043.03516); \textit{R. Pliuškevičius}, Lect. Notes Comput. Sci. 711, 640--649 (1993; Zbl 0925.03107); Lect. Notes Comput. Sci. 713, 289--300 (1993; Zbl 0793.03014); J. Math. Sci., New York 87, No. 1, 1 (1995; Zbl 0928.03021); translation from Zap. Nauchn. Semin. POMI 220, 123--144 (1995); Lect. Notes Comput. Sci. 2083, 107--120 (2001; Zbl 0988.03018); \textit{R. Pliuškevičius} and \textit{A. Pliuškevičienė}, Lect. Notes Comput. Sci. 3900, 112--128 (2006; Zbl 1235.03050); Lect. Notes Comput. Sci. 735, 299--311 (1993); J. Autom. Reason. 13, 391--407 (1994)]. The principal objective in this paper is to give a loop-type sequent calculus \(\mathbf{G}_{\mathrm{L}}\mathbf{T}\) for propositional linear temporal logic (PLTL) with temporal operators \textit{next} \(\bigcirc\)\ and \textit{henceforth always} \(\square\), denoted by \(\mathrm{PLTL}^{n,a}\), which is shown to be sound and complete. The sequent calculus \(\mathbf{G}_{\mathrm{L} }\mathbf{T}^{\mathcal{U}}\)\ for \(\mathrm{PLTL}^{n,u}\) obtained from \(\mathrm{PLTL}^{n,a}\) by adding the temporal operator \textit{until} is also considered. Construction of sound and complete cut-free sequent calculi for \(\mathrm{PLTL}\)\ is utmost problematic, which has to do with the induction principle \[ \left( \phi\wedge\square\left( \phi\supset\bigcirc\phi\right) \right) \supset\square\phi \] Some considerations on cut-free sequent calculi for PLTL in the literature go as follows: \begin{itemize} \item Infinitary sequent calculi with the \(\omega\)-type induction rule \[ \begin{array} [c]{c} \underline{\Gamma\rightarrow\Delta,\phi\quad\Gamma\rightarrow\Delta ,\bigcirc\phi\quad\dots\quad\Gamma\rightarrow\Delta,\overset{n}{\overbrace {\bigcirc\dots\bigcirc}}\phi\quad\dots}\\ \Gamma\rightarrow\Delta,\square\phi \end{array} \left( \rightarrow\square_{\omega}\right) \] were considered in [\textit{G. Sundholm}, Theoria 43, 47--51 (1977; Zbl 0364.02011); Bull. Sect. Logic, Pol. Acad. Sci. 6, 70--73 (1977; Zbl 0403.03011)]. \item Calculi with an invariant-like rule \[ \begin{array} [c]{c} \underline{\Gamma\rightarrow\Delta,I\quad I\rightarrow\bigcirc I\quad I\rightarrow\phi}\\ \Gamma\rightarrow\Delta,\square\phi \end{array} \left( \rightarrow\square_{\mathrm{I}}\right) \] were considered in [\textit{B. Paech}, Lect. Notes Comput. Sci. 385, 240--253 (1989; Zbl 0712.03015)]. \item [\textit{M. Baaz} et al., Theor. Comput. Sci. 160, No. 1--2, 241--270 (1996; Zbl 0872.68171)] gave a cut-free calculus \(\mathbf{LB}\) even for the first-order temporal logic with the weak induction principle \[ \left( \phi\wedge\bigcirc\square\phi\right) \supset\square\phi \] in place of the above full one. \end{itemize}