Local consistency of arithmetic with an ''attainability'' predicate
type: Item
instance of: scholarly article
title: Local consistency of arithmetic with an ''attainability'' predicate
zbMATH Open document ID: 0592.03047
author: E. S. Bozhich
published in: Moscow University Mathematics Bulletin
publication date: 1985-01-01T00:00:00Z
review text: Extensions of the first-order arithmetic with the predicate of feasibility had first been studied by \textit{R. Parikh} [J. Symb. Logic 36, 494-508 (1971; Zbl 0243.02037)]. By adding an axiom stating that there are natural numbers which are not attainable by successive additions of one starting from zero, one gets an inconsistent theory. However, it is still possible to show that proofs of reasonably small length yield only true arithmetical statements. The paper under review is concerned with arithmetical theories containing the attainability predicate D(x) with the meaning ''x is an attainable number'', e.g. with a theory \(PAD^+_ m(f_ 1,...,f_ k)\) whose axioms postulate: (i) D(x) determines an initial segment of the set of natural numbers closed under the successor function; (ii) the values of primitive recursive functions \(f_ 1,...,f_ k\) are attainable for any tuple of attainble arguments; (iii) m is not an attainable number. It is shown that every statement which does not include the predicate D and is provable in \(PAD^+_ m(f_ 1,...,f_ k)\) by a short proof (with respect to m) is a theorem of Peano arithmetic extended by the function symbols \(f_ i\). On the other hand, for every length l, there is a natural number m such that the statement ''the sum of any two attainable numbers is attainable'' is not provable in \(PAD^+_ m\) in l steps. A similar result is obtained for multiplication, and provability of statements in theories weaker than \(PAD^+_ m(f_ 1,...,f_ k)\) is characterized.
reviewed by: Petr Stepanek
Mathematics Subject Classification ID: 03F30
zbMATH DE Number: 3950524
zbMATH Keywords: feasibility
zbMATH Keywords: attainability predicate
zbMATH Keywords: attainable number
MaRDI profile type: Publication
Recommended article: On first-order theories with provability operator
Recommended article: Q3972528
Recommended article: Q3741624
Recommended article: Q3824311
Recommended article: Q4282618
Recommended article: About the equivalent replaceability of the double induction axiom
Recommended article: An axiomatic approach to self-referential truth
Recommended article: Q4293477
Recommended article: Q4376080
Recommended article: Finitary consistency of a free arithmetic
description: scientific article; zbMATH DE number 3950524