A conservative extension of a formal arithmetic (Q1264136)

The authors' \({\mathcal A}\) systems are sequent systems of illative \(\lambda\)-calculus, which include, as defined concepts, equality and the connectives and quantifiers. In earlier papers [the second author, Z. Math. Logik Grundlagen Math. 25, 299-314 (1979; Zbl 0423.03011); and the authors, Dokl. Akad. Nauk SSSR 250, 1310-1315 (1980; Zbl 0452.03007)] classes of N-derivations and L-derivations are defined and it is shown that an arithmetic formula A written in the language of an \({\mathcal A}\) system is derivable in formal arithmetic H\({\mathcal A}\) if and only if \(\Pi\) \(N\Rightarrow A\) has an L-derivation. The current paper claims the same result for N-derivations as a corollary to the result that a new class of derivations - \(\omega_ 1\)-derivations - forms a conservative extension of H\({\mathcal A}\). An outline of a proof of this result is given.