Finite Axiomatizability of TEIP over Open Induction

Definitions and mathematical statement

Let $T_{\mathrm{EIP}}$, also denoted $\mathrm{TEIP}$, be the first-order theory described in the supplied record as the theory of exponential integer parts of real-closed exponential fields. Let $\mathrm{IOpen}$ denote open induction: the underlying arithmetic theory together with induction for quantifier-free formulas, allowing parameters, in its intended arithmetic language. Here the exact languages, underlying arithmetic axioms, induction domain, and conventions for exponential integer parts must be those of the cited sources; the supplied record does not specify them sufficiently to give a complete independent definition of these theories.

Question. Is $\mathrm{TEIP}$ finitely axiomatizable over $\mathrm{IOpen}$? More explicitly, in the intended common first-order language $L$, does there exist a finite set $\Phi$ of $L$-sentences such that \[ \operatorname{Cn}_{L}(\mathrm{IOpen}\cup\Phi) = \operatorname{Cn}_{L}(\mathrm{TEIP})? \] Here $\operatorname{Cn}_{L}(S)$ is the set of all $L$-sentences logically entailed by $S$. Equivalently, is there a single $L$-sentence $\varphi$ such that, for every $L$-structure $M$, \[ M\models\mathrm{TEIP} \quad\Longleftrightarrow\quad M\models\mathrm{IOpen}\ \text{and}\ M\models\varphi? \] The whole open-induction theory remains available as the base; the question concerns finitely many additional axioms.

Unresolved source qualifications. The supplied original statement includes a corrupted auxiliary formula with alternating quantifiers, approximation inequalities, and product-gap inequalities. Its notation and indexing cannot be reconstructed reliably, so it is not used here to define $\mathrm{TEIP}$ or any proposed axiomatization. The displayed question precisely expresses relative finite axiomatizability, but its concrete arithmetic interpretation still requires the source definitions of $\mathrm{TEIP}$ and $\mathrm{IOpen}$.

Short English statement

Can the theory of exponential integer parts of real-closed exponential fields be obtained by adding finitely many first-order axioms to open induction? The supplied curation reports partial results while retaining this finite-axiomatizability question as open. The exact language and theory definitions require source consultation and human mathematical review.

Sources

• Local UnsolvedMath registry, supplied complete source record: permanent ID $30005751$, title Finite Axiomatizability of TEIP over Open Induction, source problem code catalogue entry, in the Oberwolfach Reports Open Problems collection. The record gives proposed year $2023$ and names no proposer.
• Supplied report citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2024), Oberwolfach Reports, pp. 3013--3061, DOI 10.4171/owr/2023/53. Supplied source URL and literature-source link labelled "original OWR report": https://doi.org/10.4171/owr/2023/53. The background describes these reports as documenting mathematical workshops and their open-problem discussions.
• Supplied literature-source link labelled "current TEIP paper": https://users.math.cas.cz/~jerabek/papers/teip.pdf. No paper title or author attribution is supplied in the record.
• Literature assessment dated exactly 2026-08-22: the supplied curation labels the problem "partially solved" and states that the 2026 primary paper still presents finite axiomatizability over $\mathrm{IOpen}$ as open while proving a strict hierarchy and related partial results. This is supplied dated curation, not an independently verified literature assessment. The supplied background explicitly requests independent verification of time-sensitive status and cited claims.
• The registry labels the statement corrected_verified and reports that it was checked against the official Oberwolfach report, preserving the report's hypotheses, notation, and open target. These are supplied verification claims; no independent source inspection is asserted here.