We discuss the problem of finding non-trivial invariants of non-deterministic, symmetric cut-reduction procedures in the classical sequent calculus. We come to the conclusion that (an enriched version of) the propositional fragment of GS4 -- i.e. the one-sided variant of Kleene's context-sharing style sequent system G4, where independent rule applications permute freely -- is an ideal framework in which to attack the problem. We show that the graph induced by axiom rules linking dual atom occurrences is preserved under arbitrary rule permutations in the cut-free fragment of GS4. We then refine the notion of axiom-induced graph so as to extend the result to derivations with cuts, and we exploit the invertibility of logical rules to define a global normalisation procedure that preserves the refined axiom-induced graphs, thus yielding a non-trivial invariant of cut-elimination in GS4. Finally, we build upon the result to devise a new proof system for classical propositional logic, where the rule permutations of GS4 reduce to identities.

翻译：本文探讨在经典序贯演算中寻找非确定性对称切割归约过程的非平凡不变量问题。我们得出结论：GS4的命题片段（即Kleene上下文共享型序贯系统G4的单边变体，其中独立规则应用可自由交换）的增强版本是解决该问题的理想框架。我们证明，在GS4的无切割片段中，由连接对偶原子出现的公理规则所诱导的图在任意规则置换下保持不变。随后我们细化公理诱导图的概念，将该结果推广至带切割的推导，并利用逻辑规则的可逆性定义全局规范化过程，该过程保持细化的公理诱导图，从而得到GS4中切割消除的非平凡不变量。最后，基于该结果我们为经典命题逻辑构建了一个新证明系统，其中GS4的规则置换被归约为恒等变换。