---
tag: Q4T4YY7XJ9
kind: concept
name: Completeness of atomic initial sequents
sources:
  - wikipedia: en:23252771@r1240943987
    locator: Completeness of atomic initial sequents
    note: adopted
    mention: wikipedia://en/23252771
    sections: [Summary]
same_as:
  wikidata: Q5156542
  wikipedia: Completeness of atomic initial sequents
inventory: [DBG0SA0FN3]
---

## Summary

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