A cut elimination theorem for stationary logic
type: Item
instance of: scholarly article
title: A cut elimination theorem for stationary logic
zbMATH Open document ID: 0633.03051
DOI: 10.1016/0168-0072(87)90080-7
published in: Annals of Pure and Applied Logic
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03C75
Mathematics Subject Classification ID: 03C80
zbMATH DE Number: 4029550
zbMATH Keywords: complete cut-free labelled sequent calculus
zbMATH Keywords: stationary logic
zbMATH Keywords: subformula property
zbMATH Keywords: interpolation
author: Manfred E. Szabo
MaRDI profile type: Publication
full work available at URL: 0168-0072(87)90080-7
OpenAlex ID: W2084909717
cites work: Stationary logic
cites work: A correction to “stationary logic”
cites work: New axiomatizations for logics with generalized quantifiers
cites work: Logic with the quantifier “there exist uncountably many”
cites work: Generalized Quantifiers and Compact Logic
cites work: Q5610986
cites work: Proof theory
description: scientific article; zbMATH DE number 4029550