View in EDS

Analogues of Shepherdson's Theorem for a language with exponentiation.

Saved in:
Bibliographic Details
Title: Analogues of Shepherdson's Theorem for a language with exponentiation.
Authors: Kovalyov, Konstantin1 (AUTHOR)
Source: Journal of Logic & Computation. Apr2026, Vol. 36 Issue 3, p1-38. 38p.
Subjects: Exponentiation, Semirings (Mathematics), Mathematics theorems, Mathematical inequalities, Integers, Mathematical induction
Abstract: In 1964, Shepherdson (1964, Bull. Pol. Acad. Sci. 12) proved that a discretely ordered semiring M + satisfies IOpen (quantifier-free induction) iff the corresponding ring M is an integer part of a model of the theory of real closed fields (RCF). In this paper, we consider open induction schema in the language of arithmetic expanded by exponentiation or by the power function and try to find similar criteria for models of these theories. For several recursively axiomatized extensions T of the theory of RCF, we obtain analogues of Shepherdson's Theorem in the following sense: If an exponential field R is a model of T and a discretely ordered ring (DOR) M is an exponential integer part of R ⁠ , then M + is a model of open induction in the expanded language. The proof of the opposite implication—that for any model M of open induction in the expanded language there exists an exponential field R ⊨ T such that M is an exponential integer part of R —remains, in general, an open question. However, we isolate a natural sufficient condition, related to the well-known Bernoulli inequality, under which this result holds. We define a finite extension T of the usual open induction so that, for any DOR M ⁠ , the semiring M + satisfies T iff there is an exponential RCF R with the inequality exp ⁡ (x) ⩾ 1 + x such that M is an exponential integer part of R ⁠. Using these results, we obtain some concrete independence results for these theories. [ABSTRACT FROM AUTHOR]
Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
Abstract:In 1964, Shepherdson (1964, Bull. Pol. Acad. Sci. 12) proved that a discretely ordered semiring M + satisfies IOpen (quantifier-free induction) iff the corresponding ring M is an integer part of a model of the theory of real closed fields (RCF). In this paper, we consider open induction schema in the language of arithmetic expanded by exponentiation or by the power function and try to find similar criteria for models of these theories. For several recursively axiomatized extensions T of the theory of RCF, we obtain analogues of Shepherdson's Theorem in the following sense: If an exponential field R is a model of T and a discretely ordered ring (DOR) M is an exponential integer part of R ⁠ , then M + is a model of open induction in the expanded language. The proof of the opposite implication—that for any model M of open induction in the expanded language there exists an exponential field R ⊨ T such that M is an exponential integer part of R —remains, in general, an open question. However, we isolate a natural sufficient condition, related to the well-known Bernoulli inequality, under which this result holds. We define a finite extension T of the usual open induction so that, for any DOR M ⁠ , the semiring M + satisfies T iff there is an exponential RCF R with the inequality exp ⁡ (x) ⩾ 1 + x such that M is an exponential integer part of R ⁠. Using these results, we obtain some concrete independence results for these theories. [ABSTRACT FROM AUTHOR]
ISSN:0955792X
DOI:10.1093/logcom/exag013