In
sequent calculus, the completeness of atomic initial sequents states that initial sequents (where is an arbitrary formula) can be derived from only atomic initial sequents (where is an
atomic formula). This theorem plays a role analogous to
eta expansion in
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
, and dual to
cut-elimination and
beta reduction. Typically it can be established by induction on the structure of , 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
Anne Sjerp Troelstra (10 August 1939 – 7 March 2019) was a professor of pure mathematics and foundations of mathematics at the Institute for Logic, Language and Computation (ILLC) of the University of Amsterdam.
He was a Constructivism (mathem ...
and
Helmut Schwichtenberg
Helmut Schwichtenberg (born 5 April 1942 in Żagań) is a German mathematical logician.
Schwichtenberg studied mathematics from 1961 at the FU Berlin and from 1964 at the University of Münster, where he received his doctorate in 1968 from D ...
. ''Basic Proof Theory''. Edition: 2, illustrated, revised. Published by Cambridge University Press, 2000.
Theorems in the foundations of mathematics
Proof theory
{{mathlogic-stub