Completeness of atomic initial sequents

In sequent calculus, the completeness of atomic initial sequents states that initial sequents AA (where A is an arbitrary formula) can be derived from only atomic initial sequents pp (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

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