The book is devoted to one of the main sections of mathematical logic - proof theory. In addition to the traditional results on first-order systems, such as the eliminability of the section and the completeness of the intuitionistic and classical calculus of predicates, the incompleteness and consistency of arithmetic, the book cites recent achievements in this area, including proofs of the eliminability of sections in simple type theory and the consistency of a limited part of mathematical analysis.