arxiv: 2605.01636 · v1 · submitted 2026-05-02 · 🧮 math.LO · cs.LO

Recognition: 3 theorem links

· Lean Theorem

Inexpressibility in Exp-Minus-Log

Mark Carney

Pith reviewed 2026-05-08 19:24 UTC · model grok-4.3

classification 🧮 math.LO cs.LO

keywords EMLcomputabilityChaitin's Omegainexpressibilityelementary functionsEL numbersreal numberslogic

0 comments

The pith

Every number expressible from 1 using the binary operation E equals exp minus log is computable, and Chaitin's Omega lies outside this class.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper investigates what real numbers can be obtained in the Exp-Minus-Log system introduced by Odrzywolek. This system starts with the constant 1 and applies only the two-argument function E(alpha, beta) equals exp(alpha) minus log(beta). It establishes that every such constructible number must be computable. The argument then isolates Chaitin's Omega as a concrete non-computable real that cannot be reached by any finite sequence of these operations. The result therefore supplies an explicit inexpressibility theorem for the system, which the paper notes is equivalent to Chow's earlier EL numbers.

Core claim

Every EML-expressible number is computable. In particular, the canonical non-computable real Omega_U cannot be obtained from the constant 1 by any finite number of applications of the binary operation E.

What carries the argument

EML-expressibility: the smallest set of complex numbers containing the constant 1 and closed under the binary operation E(alpha, beta) = exp(alpha) - log(beta).

If this is right

The EML system cannot define any non-computable real.
Chaitin's Omega lies strictly outside the numbers obtainable from exp and log reductions in this manner.
Any number proven expressible in EML must admit a computable approximation to arbitrary precision.
The equivalence with Chow's EL numbers transfers the same computability bound to that earlier formulation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Other information-theoretic constants with halting-problem encodings are likely to share the same inexpressibility.
The result may help classify which familiar mathematical constants fall inside or outside the EML closure.
It supplies a concrete test for whether a proposed closed-form expression for a real number stays within elementary reductions of this type.

Load-bearing premise

That the inductive definition using only the constant 1 and the single operation E fully captures the intended class of expressible numbers.

What would settle it

An explicit finite expression for Chaitin's Omega_U built from the constant 1 by repeated applications of E, or a demonstration that Omega satisfies an algebraic or analytic relation allowing it to be recovered inside the EML closure.

read the original abstract

Odrzywo\l{}ek defined a system Exp-Minus-Log (EML) that reduces all elementary functions over complex numbers down to a constant `$1$', and a single two place function $E(\alpha, \beta) = \exp(\alpha) - \log(\beta)$. This paper shows that in this system, equivalent to Chow's EL numbers, every EML-expressible number is computable. We go on to prove that the canonical example of a non-computable real, Chaitin's $\Omega_U$, is inexpressible in EML. This gives a formal inexpressibility theorem for this system.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper shows Omega is inexpressible in EML because all such numbers are computable by a basic induction on the term structure.

read the letter

This paper shows that Chaitin's Omega is inexpressible in the Exp-Minus-Log system. All numbers you can form starting from 1 and closing under E(α, β) = exp(α) - log(β) turn out to be computable. It does well by giving an explicit inexpressibility theorem for this minimal system, linking it to prior work on EL numbers. The proof uses a straightforward induction on term depth to establish computability at each step. This separates the computable reals from non-computable ones inside the system in a formal way. The induction works because 1 is computable and both exp and log preserve computability on their domains. Since Omega is known to be non-computable, it cannot be expressed this way. This avoids any circularity and rests on standard computability facts rather than any self-referential constructions inside the paper. A soft spot is that the result is quite direct once you look at the inductive definition. It doesn't require heavy machinery, which is a strength for clarity but means the novelty is mainly in the application to EML rather than a surprising new technique. The equivalence to Chow's numbers is noted but not central to the computability argument, as the induction stands on its own. This is for specialists in mathematical logic and computable analysis who care about what can be expressed with limited operations. It is worth sending to peer review because the claim is precise and the reasoning appears sound. A reader would get a clear example of how minimal function systems can still capture only computable numbers.

Referee Report

0 major / 3 minor

Summary. The manuscript defines the Exp-Minus-Log (EML) system via the constant 1 and the binary operation E(α, β) = exp(α) − log(β), establishes its equivalence to Chow's EL numbers, proves by induction on term depth that every EML-expressible number is computable, and concludes that Chaitin's Ω_U is inexpressible in EML since it is non-computable.

Significance. If the central claims hold, the paper supplies a clean, parameter-free separation between computable reals and a canonical non-computable real inside a minimal system for elementary functions. The inductive argument on term depth is a standard and fully rigorous method that directly yields the inexpressibility result without additional assumptions.

minor comments (3)

[Abstract] Abstract: the two main theorems are stated without any indication of the inductive proof strategy or domain considerations for log; a single sentence summarizing the induction would improve accessibility.
The claimed equivalence to Chow's EL numbers is used to identify the class but is not required for the computability or inexpressibility arguments; a brief self-contained justification or precise citation would still aid readers.
The manuscript should explicitly note that the inductive argument assumes all intermediate terms respect the domain of log (i.e., positive second arguments); while this does not affect the final claim, it clarifies the well-definedness of the set.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of the manuscript and for noting that the inductive argument on term depth is standard and fully rigorous. The recommendation for minor revision is appreciated, but the report lists no specific major comments to address.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper defines EML-expressibility directly via inductive closure: constant 1 together with the binary operation E(α, β) = exp(α) − log(β). It then shows by induction on term depth that every closed term evaluates to a computable real, relying only on the standard fact that exp and log are computable functions (with effective approximations on appropriate domains). Chaitin’s Ω_U is independently known to be non-computable, hence lies outside the class. The parenthetical reference to equivalence with Chow’s EL numbers serves only to name the class and is not invoked in the computability or inexpressibility arguments. No step reduces by construction to a fitted parameter, self-definition, or load-bearing self-citation; the chain rests on external, independently verifiable facts about computability.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the standard definition of EML expressions, the equivalence to Chow's EL numbers, and background facts from computability theory; no free parameters or invented entities are introduced.

axioms (2)

standard math Standard algebraic and analytic properties of exp and log over the complex numbers
Invoked to define the binary operation E(α, β).
domain assumption Equivalence of EML to Chow's EL numbers
Stated in the abstract as the setting for the expressibility results.

pith-pipeline@v0.9.0 · 5389 in / 1279 out tokens · 96045 ms · 2026-05-08T19:24:23.498389+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AlphaCoordinateFixation.lean J_uniquely_calibrated_via_higher_derivative unclear
Define [[·]] : E → C recursively: [[1]] = 1, [[E(α,β)]] = exp([[α]]) − log([[β]]).
IndisputableMonolith/Foundation/ArithmeticFromLogic.lean embed_injective unclear
By Theorem 2, EML_R ⊆ Comp_R, and by Theorem 1, Ω_U ∈ R \ Comp_R. Hence Ω_U ∉ EML_R.
IndisputableMonolith/Foundation/BranchSelection.lean branch_selection unclear
By induction on φ ... [[E(α,β)]] = exp([[α]]) − log([[β]]) is computable.

Reference graph

Works this paper leans on

7 extracted references · 5 canonical work pages · 1 internal anchor

[1]

All elementary functions from a single binary operator

Odrzywo. All elementary functions from a single binary operator , publisher =. 2026 , copyright =. doi:10.48550/ARXIV.2603.21852 , url =

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2603.21852 2026
[2]

, year =

Chow, Timothy Y. , year =. What Is a Closed-Form Number? , volume =. The American Mathematical Monthly , publisher =. doi:10.1080/00029890.1999.12005066 , number =

work page doi:10.1080/00029890.1999.12005066 1999
[3]

, year =

Chaitin, Gregory J. , year =. A Theory of Program Size Formally Identical to Information Theory , volume =. Journal of the ACM , publisher =. doi:10.1145/321892.321894 , number =

work page doi:10.1145/321892.321894
[4]

Computable Analysis: An Introduction , ISBN =

Weihrauch, Klaus , year =. Computable Analysis: An Introduction , ISBN =. doi:10.1007/978-3-642-56999-9 , journal =

work page doi:10.1007/978-3-642-56999-9
[5]

Algorithmic randomness and complexity

Downey, Rodney G and Hirschfeldt, Denis R. Algorithmic randomness and complexity
[6]

Some undecidable problems involving elementary functions of a real variable , volume =

Richardson, Daniel , year =. Some undecidable problems involving elementary functions of a real variable , volume =. Journal of Symbolic Logic , publisher =. doi:10.2307/2271358 , number =

work page doi:10.2307/2271358
[7]

M\"unster Journal of Mathematics , volume =

Katrin Tent and Martin Ziegler , title =. M\"unster Journal of Mathematics , volume =