Extension without cut
The extension rule introduces a new propositional variable \(x\) denoting formula \(A\) by adding \(A\to x\) and \(x\to A\). The author claims that ``there is no such thing as a cut-free extended Frege system''. He defines cut-free extension systems for deep inference.
scientific article; zbMATH DE number 6092975
scientific article