Completeness of atomic initial sequents
In sequent calculus, the completeness of atomic initial sequents states that initial sequents A ⊢ AScript error: No such module "Check for unknown parameters". (where AScript error: No such module "Check for unknown parameters". is an arbitrary formula) can be derived from only atomic initial sequents p ⊢ pScript error: No such module "Check for unknown parameters". (where pScript error: No such module "Check for unknown parameters". 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 AScript error: No such module "Check for unknown parameters"., 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.