The eliminability of sections ( Genzen's theorem , elimination theorem ) is a property of logical calculi, according to which any sequence deduced in this calculus can be deduced without applying the section rule [1] . It plays a fundamental role in the theory of evidence and an important methodological role in mathematical logic as a whole in connection with the fact that it provides a constructive method for proving consistency , in particular, for classical and intuitionistic first-order logics [2] .
For the classical and intuitionistic calculus of sequences, the property was proved by Genzen in 1934 . In 1953, Takeuchi conjecture was put forward , according to which the removability of sections takes place for a simple type theory and higher order logics corresponding to it, later it found confirmation - for classical second-order logic, proved the removability of sections, for Takahashi and for simple type theory , evidence was soon found for a series of non-classical theories of higher orders ( Dragaline ) and developed type theories ( for system F ).
Symbolic wording: let and - provable calculus sequences ; if - sequence of calculus then it is provable [3] .
Notes
- ↑ Evidence Theory, 1978 , p. 29.
- ↑ Elimination Theorem / P. I. Bystrov // New Philosophical Encyclopedia : in 4 volumes / prev. scientific ed. Council V. S. Styopin . - 2nd ed., Rev. and add. - M .: Thought , 2010 .-- 2816 p.
- ↑ Ershov, 1987 , p. 214.
Literature
- G. Gentzen. Untersuchungen über das logische Schließen (German) // Mathematische Zeitschrift. - 1934-1935. - Bd. 39 . - S. 405-431 . - DOI : 10.1007 / BF01201363 .
- Takeuchi G. Theory of evidence. - M .: Mir, 1978.- 412 p.
- Ershov Yu. L. , Palyutin E.A. Mathematical logic. - M .: Nauka, 1987 .-- 336 p.