A conservative extension of a formal arithmetic
type: Item
instance of: scholarly article
title: A conservative extension of a formal arithmetic
zbMATH Open document ID: 0689.03006
author: A. A. Kuzichev
author: A. S. Kuzichev
published in: Moscow University Mathematics Bulletin
publication date: 1988-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 4128786
zbMATH Keywords: sequent systems of illative \(\lambda \) -calculus
zbMATH Keywords: formal arithmetic
zbMATH Keywords: derivations
zbMATH Keywords: conservative extension
reviewed by: Martin W. Bunder
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 4128786