A conservative extension of a formal arithmetic (Q1264136)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A conservative extension of a formal arithmetic |
scientific article |
Statements
A conservative extension of a formal arithmetic (English)
0 references
1988
0 references
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.
0 references
sequent systems of illative \(\lambda \) -calculus
0 references
formal arithmetic
0 references
derivations
0 references
conservative extension
0 references