A cut elimination theorem for stationary logic (Q1095904)

We develop a complete cut-free labelled sequent calculus for stationary logic and prove that in the given formalization, this logic has the subformula property. The necessary parameter restrictions on the rules of inference involved explain the compatibility of this result with the known failure of interpolation for stationary logic. The methods employed in this paper are those of \textit{J. Barwise}, \textit{M. Kaufmann} and \textit{M. Makkai} [Ann. Math. Logic 13, 171-224 (1978; Zbl 0372.02031) and ibid. 20, 231-232 (1981; Zbl 0457.03034)] and \textit{G. Gentzen} [The collected papers of Gerhard Gentzen (M. E. Szabo (ed.)) (1969; Zbl 0209.300)], augmented with suitable permutation rules for first and second order quantifiers.