Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the theory of exponential integer parts

Emil Jeřábek

TL;DR

The work addresses the problem of axiomatizing exponential integer parts (EIP) of real-closed exponential fields from several logical languages. It introduces the TEIP framework in the base language $\mathcal{L}_{\mathrm{OR}}$ via the PowG game, and in extended languages with $2^x$ and with $P_2$, proving TEIP is a proper extension of $IOpen$ and establishing conservativity results between languages through back-and-forth constructions and recursive-saturation techniques. It also analyzes the PowG game to derive upper and lower bounds on the minimal winning rounds $c(u)$, linking these bounds to arithmetical structure of starting values and providing explicit families with tight bounds. The oddless interpretation relates TEIP_{P_2} and TEIP_{Pow2} to standard bounded arithmetic theories, showing non-uniqueness phenomena and giving conditions for when expansions are unique. Overall, the paper clarifies the logical strength of EIP in real-closed exponential contexts and connects algebraic properties of the exponential function to bounded-arithmetic frameworks, with several open questions about finite axiomatizability and exact conservativity relations.

Abstract

We axiomatize the first-order theories of exponential integer parts of real-closed exponential fields in a language with $2^x$, in a language with a predicate for powers of 2, and in the basic language of ordered rings. In particular, the last theory extends IOpen by sentences expressing the existence of winning strategies in a certain game on integers; we show that it is a proper extension of IOpen, and give upper and lower bounds on the required number of rounds needed to win the game.

On the theory of exponential integer parts

TL;DR

The work addresses the problem of axiomatizing exponential integer parts (EIP) of real-closed exponential fields from several logical languages. It introduces the TEIP framework in the base language via the PowG game, and in extended languages with and with , proving TEIP is a proper extension of and establishing conservativity results between languages through back-and-forth constructions and recursive-saturation techniques. It also analyzes the PowG game to derive upper and lower bounds on the minimal winning rounds , linking these bounds to arithmetical structure of starting values and providing explicit families with tight bounds. The oddless interpretation relates TEIP_{P_2} and TEIP_{Pow2} to standard bounded arithmetic theories, showing non-uniqueness phenomena and giving conditions for when expansions are unique. Overall, the paper clarifies the logical strength of EIP in real-closed exponential contexts and connects algebraic properties of the exponential function to bounded-arithmetic frameworks, with several open questions about finite axiomatizability and exact conservativity relations.

Abstract

We axiomatize the first-order theories of exponential integer parts of real-closed exponential fields in a language with , in a language with a predicate for powers of 2, and in the basic language of ordered rings. In particular, the last theory extends IOpen by sentences expressing the existence of winning strategies in a certain game on integers; we show that it is a proper extension of IOpen, and give upper and lower bounds on the required number of rounds needed to win the game.
Paper Structure (7 sections, 26 theorems, 67 equations)

This paper contains 7 sections, 26 theorems, 67 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Exponential integer parts in a language with $2^x$ or $P_2$
  4. Exponential integer parts in $\mathcal{L}_{\mathrm{OR}}$
  5. Analysis of $\mathrm{PowG}$
  6. Oddless interpretation
  7. Discussion

Key Result

Theorem 2.1

An $\mathcal{L}_{\mathrm{OR}}$-structure $\mathfrak M$ is an IP of a RCF if and only if $\mathfrak M_{\ge0}\vDash\mathsf{IOpen}$. $\Box$

Theorems & Definitions (42)

  • Theorem 2.1: Shepherdson sheph
  • Theorem 2.2
  • Lemma 2.3: Barwise and Schlipf bar-sch
  • Definition 3.1
  • Theorem 3.2
  • Definition 3.3
  • Lemma 3.4
  • Lemma 3.5
  • Definition 3.6
  • Lemma 3.7
  • ...and 32 more