Sequential Modification of Constructive Logic Calculus for Normal Formulas without Structural Deduction Rules

Abstract

It is known that traditional constructive (intuitionistic in the terminology of some authors) predicate calculus turns out to be inadequate for a formalized exposition of even the very initial chapters of constructive mathematical analysis, and it is necessary to go beyond the scope of this calculus. In this respect, more satisfactory are such constructive logic calculi in which the steps of the algorithm of constructive determination of the mathematical inferences, the methods of operating with conditional equalities of terms and the concept of comprehensibility of terms, the methods of insertion and elimination of subordinate variables, etc. are formalized (see [1], [2]). One of the modifications of such a constructive logic calculus, the calculus NK ^Σ₁ was introduced and investigated by A. V. Idel’son in [3]. A. V. Idel’son reduced the question of a foundation for the calculus NK ^Σ₁ to the foundation for a considerably simpler calculus NN₁ in whose language only normal formulas without subordinate variables can be constructed (Theorem 12.3.1 from [3]).

The principal results of this note were presented to the Leningrad Seminar on Mathematical Logic on June 24, 1966 and October 14, 1966.