Completeness of atomic initial sequents

In sequent calculus, the completeness of atomic initial sequents states that initial sequents $A ⊢ A$ (where $A$ is an arbitrary formula) can be derived from only atomic initial sequents $p ⊢ p$ (where $p$ is an atomic formula). This theorem plays a role analogous to eta expansion in lambda calculus, and dual to cut-elimination and beta reduction. Typically it can be established by induction on the structure of $A$ , much more easily than cut-elimination.

References

Gaisi Takeuti. Proof theory. Volume 81 of Studies in Logic and the Foundation of Mathematics. North-Holland, Amsterdam, 1975.
Anne Sjerp Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Edition: 2, illustrated, revised. Published by Cambridge University Press, 2000.

This article is issued from Wikipedia - version of the 10/18/2011. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.