View source for Completeness of atomic initial sequents

In [[sequent calculus]], the '''completeness of atomic initial sequents''' states that initial sequents {{math|<VAR>A</VAR> ⊢ <VAR>A</VAR>}} (where {{math|<VAR>A</VAR>}} is an arbitrary [[formula (logic)|formula]]) can be derived from only atomic initial sequents {{math|<VAR>p</VAR> ⊢ <VAR>p</VAR>}} (where {{math|<VAR>p</VAR>}} 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 [[structural induction|induction on the structure]] of {{math|<VAR>A</VAR>}}, 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.

[[Category:Theorems in the foundations of mathematics]]
[[Category:Proof theory]]

{{mathlogic-stub}}