Proof-theoretical investigation of temporal logic with time gaps (Q5930981): Difference between revisions

A first-order intuitionistic temporal logic sequent calculus is considered, which is based on an intuitionistic version of the first-order sequent calculus LJ without structural rules, and endowed with extra rules for handling temporal operators, in the style of the system LB introduced by \textit{M. Baaz, A. Leitsch} and \textit{R. Zach} [Theor. Comput. Sci. 160, 241-270 (1996; Zbl 0872.68171)]. For the system introduced by the author, called LBJ, the invertibility of some of the rules is proved, together with the syntactic admissibility of the structural rules and the cut rule. Versions of Harrop's theorem and Craig's interpolation theorem are proved. Finally, a Gentzen midsequent theorem is proved for the weaker system obtained by removing the antecedent disjunction rule.