Towards a semantic characterization of cut-elimination (Q817704)

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.