Extension without cut (Q714731)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Extension without cut |
scientific article |
Statements
Extension without cut (English)
0 references
11 October 2012
0 references
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.
0 references
deep inference
0 references
Frege systems
0 references
proof complexity
0 references
cut elimination
0 references
propositional pigeonhole principle
0 references
balanced tautologies
0 references
0 references
0 references
