Towards a semantic characterization of cut-elimination
type: Item
instance of: scholarly article
title: Towards a semantic characterization of cut-elimination
zbMATH Open document ID: 1105.03057
author: Agata Ciabattoni
author: Kazushige Terui
published in: Studia Logica
publication date: 2006-03-17T00:00:00Z
review text: An occurrence of the cut rule in a derivation is called reductive if either (i) both cut formulas are the principal formulas of logical rules, or (ii) one of the two cut formulas is a context formula of a rule other than the cut, or (iii) one of the two premises is an identity axiom (of the form \(X\Rightarrow X\)). Reductive cut-elimination for simple theories has been given a syntactic and a semantic characterization in the paper under review. A sequent calculus is called simple, if it is a single-conclusion calculus that contains some identity axioms (mentioned above), the cut rule, structural rules, and left and right logical rules for each logical connective. The syntactic characterization reads as: a simple theory admits reductive cut-elimination iff (1) its logical rules are reductive, i.e., if \(\Theta\Rightarrow A\) is deducible from \textbf{S}, and \(\Theta_1,A,\Theta_2\Rightarrow B\) is deducible from \({\mathbf S}'\), then \(\Theta_1,\Theta,\Theta_2\Rightarrow B\) is deducible from \(\{{\mathbf S},{\mathbf S}'\}\) using only the identity axioms, the cut rule, and the structural rules; and (2) its structural rules are weakly substitutive, i.e., every instance of any of them is derivable within the calculus. Also a semantic variant of the above characterization is presented (for reductive cut-elimination) in terms of pre-phase structures.
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B47
zbMATH DE Number: 5013038
zbMATH Keywords: sequent calculus
zbMATH Keywords: cut-elimination
zbMATH Keywords: nonclassical logics
zbMATH Keywords: substructural logics
zbMATH Keywords: phase semantics
reviewed by: Saeed Salehi
MaRDI profile type: MaRDI publication profile
full work available at URL: s11225-006-6607-2
OpenAlex ID: W2166144087
cites work: Non‐commutative intuitionistic linear logic
cites work: Q4539639
cites work: Algebraic aspects of cut elimination
cites work: Display logic
cites work: Q4215630
cites work: Computer Science Logic
cites work: Untersuchungen über das logische Schliessen. I
cites work: Q4128539
cites work: Q3773876
cites work: Q3994895
cites work: Q4263837
cites work: Extending intuitionistic linear logic with knotted structural rules
cites work: Q4412848
cites work: Q4222841
cites work: Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
cites work: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
cites work: Q4940727
cites work: Bounded contraction and Gentzen-style formulation of Łukasiewicz logics
cites work: Q4805593
cites work: Q4499084
cites work: Which structural rules admit cut elimination? An algebraic criterion
DOI: 10.1007/S11225-006-6607-2
description: scientific article; zbMATH DE number 5013038