A SEMANTIC INSIGHT INTO CUT ELIMINATION
Alexej P. Pynko · 2025
A Cut-/Reflexivity-free version LK −C/R of the propositional fragment of Gentzen calculus LK for the classical propositional logic P C endowed with propositional rules inverse to its logical ones as well as rules of constant elimination is proved to be equivalent to the bounded version of the "logic of paradox"/"Kleene three-valued logic" (LP/K3) 01 under the standard interpretation of propositional sequents by propositional clauses and inverse interpretation of propositional formulas by premise-less single-conclusion sequents, "with same theorems as P C, implying that LK has same derivable sequents as LK − , and so yielding a new semantic insight into Cut Elimination in LK"/. As a by-product of the discovered equivalence and absence of proper consistent extensions of (LP/K3) 01 other than P C "and that relatively axiomatized by the Ex Contradictione Quodlibet rule"/, proved here upon the basis of the universal algebraic technique elaborated in an earlier work of ours, we prove that LK −C/R has no proper consistent extension other than LK "and the one relatively axiomatized by the context-free restriction of Cut"/.