Pith. sign in

REVIEW 3 major objections 6 minor 11 references

Computable presentations of randomizations

T0 review · 3 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

Pith's one-line read Countable classical structures are decidable exactly when their Borel randomizations have aware computable presentations, and effectively ω-categorical structures yield computably categorical randomizations.

desk verdict Effective randomization paper with real new results, a few repairable glitches; worth refereeing. read the letter →

arxiv 2506.06187 v1 pith:T4XBP2ZF submitted 2025-06-06 math.LO

classification math.LO MSC 03C5703C66
keywords Borelrandomizationcomputablepresentationdecidableeffectivemetricstructuretheorycategoricityatomlessprobabilityalgebraquantifiereliminationcontinuouslogic
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper analyzes the Borel randomization $\mathcal{M}^{[0,1)}$ of a countable classical structure $\mathcal{M}$, whose first sort consists of $\mathcal{M}$-valued random variables and whose second sort is the probability algebra of $[0,1)$. Its central claim is that $\mathcal{M}$ has a decidable presentation if and only if $\mathcal{M}^{[0,1)}$ has a computable presentation that is aware, i.e. the constant random variables are uniformly computable points. This connects classical decidability of structures with computability in continuous metric structures. The paper further claims that effective $\omega$-categoricity of $\mathcal{M}$ makes $\mathcal{M}^{[0,1)}$ computably categorical, with the atomless probability algebra as a special case, and that every randomization has effective quantifier elimination uniformly in the language.

What carries the argument

The load-bearing object is the Borel randomization $\mathcal{M}^{[0,1)}$, a two-sorted continuous structure whose $K$-sort contains Borel $\mathcal{M}$-valued random variables and whose other sort is the probability algebra $\mathcal{B}([0,1))$, with an event symbol $J\varphi K$ for each classical formula $\varphi$. The technical core is an induced-presentation correspondence: presentations of $\mathcal{M}$ and aware presentations of $\mathcal{M}^{[0,1)}$ convert into each other, with the randomization's computable presentation being automatically decidable. The categoricity proof runs a back-and-forth that realizes isolating types in c.e. closed sets, while the quantifier-elimination proof uses a definable-family notion for metric structures and an effective test that removes quantifiers one at a time.

What would settle it

Find a countable classical structure $\mathcal{M}$ with no decidable presentation such that $\mathcal{M}^{[0,1)}$ has an aware computable presentation; that would contradict Theorem 3.5 directly, and if the computable presentation is non-aware it would show the awareness assumption is essential.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is an equivalence: for a countable classical structure $\mathcal{M}$, there is a decidable presentation of $\mathcal{M}$ precisely when there is an aware computable presentation of the Borel randomization $\mathcal{M}^{[0,1)}$. The forward direction is constructive: a decidable presentation of $\mathcal{M}$ induces a computable aware presentation of the randomization via simple functions with rational-interval indicators. The reverse direction recovers a presentation of $\mathcal{M}$ from an aware presentation by reading off the unique constant random variable inside small rational balls, and then uses the randomization's effective quantifier elimination to decide all formulas. Under effective $\omega$-categoricity, the same toolkit produces a computable isomorphism between any two computable presentations of $\mathcal{M}^{[0,1)}$, making it computably categorical.

Load-bearing premise

The load-bearing premise is that $\mathcal{B}([0,1))$ is countably saturated, which the back-and-forth proofs invoke as 'By countable saturation' without supplying a proof; if that saturation fails, the constructed partial elementary maps need not extend to genuine isomorphisms.

Editorial extensions

If this is right

  • A decidable presentation of $\mathcal{M}$ yields a computable (hence decidable) presentation of $\mathcal{M}^{[0,1)}$, and an aware computable presentation of $\mathcal{M}^{[0,1)}$ yields a decidable presentation of $\mathcal{M}$.
  • For effectively recognizable structures, such as computably presentable real closed fields or expansions of $\mathcal{M}$ by constants, the awareness condition can be dropped from the equivalence.
  • If $\mathcal{M}$ is effectively $\omega$-categorical, then $\mathcal{M}^{[0,1)}$ has exactly one computable presentation up to computable isomorphism; for the two-element set this says the atomless probability algebra is computably categorical.
  • Every randomization has effective quantifier elimination with an algorithm depending only on the classical language $L$, so any computable presentation of a randomization is automatically a decidable presentation.
  • Since $\mathcal{M}^{[0,1)} \cong \mathcal{N}^{[0,1)}$ forces $\mathcal{M} \cong \mathcal{N}$, randomization cannot manufacture a computable presentation of a non-decidable structure from a decidable one.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The induced-presentation correspondence suggests a general recipe: any continuous structure built from a classical structure by adding a probability-algebra sort will inherit decidability exactly when constants are effectively accessible, a pattern that may extend beyond Borel randomizations.
  • If every computable presentation of a randomization turned out to be aware, the main equivalence would hold with no extra hypothesis; the paper leaves this as an explicit open question.
  • Because effective quantifier elimination is uniform in the language, expansions and reducts of randomizations should inherit feasible presentations without reproving the elimination, which could make randomization a practical tool for building computable metric structures.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper develops the effective metric model theory of Keisler randomizations. For a countable classical structure M, the Borel randomization M^{[0,1)} is treated as a two-sorted continuous metric structure whose K-sort consists of M-valued random variables and whose B-sort is the atomless probability algebra. The main results are: (1) M has a decidable presentation iff M^{[0,1)} has an 'aware' computable presentation (Theorem 3.5); (2) if M is effectively recognizable, awareness can be dropped; (3) if M is effectively ω-categorical, then M^{[0,1)} is computably categorical, with the atomless probability algebra as a special case (Theorems 4.4 and 4.9); and (4) every randomization theory has effective quantifier elimination, uniformly in the underlying classical language (Theorem 5.2). The paper also defines effective versions of c.e. closed sets and definable families, which are used in the proofs.

Significance. The results are a good first step in an effective theory of randomizations. The equivalence in Theorem 3.5 is natural and non-obvious, and the use of awareness to bridge decidable presentations of M with computable presentations of M^{[0,1)} is elegant. The computable categoricity of the atomless probability algebra is a result of independent interest, and the back-and-forth strategy is likely to generalize. The effective quantifier elimination theorem is a genuine contribution: it supplies the first systematic treatment of effective QE in continuous logic and does so uniformly in the language and independently of M. The paper is self-contained in its main technical lines and gives explicit effective constructions, which makes the remaining gaps local and repairable.

major comments (3)
  1. [Section 2.3, Lemma 2.5] The criterion for B(f;ε)∩M≠∅ is stated as the existence of indices j_1,...,j_t with a_{j_1}=...=a_{j_t} and Σ μ(I_{j_p})>ε. With the induced simple functions taken to partition [0,1), d(f,a)=1−μ([f=a]), so the correct condition is Σ_{j:a_j=a} μ(I_j)>1−ε. The condition in the paper is weaker and will in general certify balls that contain no constant function, so this proof does not establish that the induced presentation is aware. Replace ε by 1−ε (and either state that the I_j partition [0,1) or add an explicit complement piece to the simple function).
  2. [Section 4, Lemma 4.2] The search condition ψ_p(D,A_δ)+δ < (ε−d(C,D))/(2|A|) is used to invoke Lemma 4.1 with error ε−d(C,D). Lemma 4.1 requires ψ_p(D,A)<(ε−d(C,D))/n, where n=2^m and m=|A|. Since 2m<n for m≥3, the displayed threshold is weaker than the one supplied by Lemma 4.1, so the algorithm can enumerate a ball B(C,ε) that does not actually meet the set of realizations of p. The soundness part of the proof therefore fails; the denominator should be n=2^m (the same correction is needed in the subsequent 'we now need to verify' paragraph, where the bound η/(2|A|) appears again).
  3. [Section 4, Theorem 4.4] The back-and-forth extension step invokes 'By countable saturation, p is realized in B([0,1))' without proof or citation. The type p is a 1-type over a finite tuple, so countable saturation is both unproved and stronger than needed; moreover, the paper does not show that the atomless probability algebra is countably saturated. Since the extension of partial elementary maps depends on realizing p, the proof of computable categoricity is incomplete as written, and through Proposition 2.9/2.10 this gap affects the converse of Theorem 3.5. The repair is to state and prove an explicit lemma: over a finite tuple A_1,...,A_m, every consistent 1-type is realized by choosing the required measure inside each atom of the finite algebra generated by the tuple. The analogous finite-type realization step for M^{[0,1)} in Theorem 4.9 should be stated and justified, e.g. via Fact 5.10.
minor comments (6)
  1. [Section 3, Example 3.8(1)] Not every computably presentable real closed field is effectively recognizable, because a transcendental element is not definable in the language of ordered fields; the claim holds only for real closed fields in which every element is algebraic (e.g. the real algebraic numbers).
  2. [Section 5, Lemma 5.5] In the proof, 'Given a restricted function v' should read 'Given a computable continuous function u, enumerate restricted functions v', and 'if ν is such that' should be 'if v is such that'.
  3. [Section 5, Theorem 5.2] In the paragraph beginning 'Let θ_j', the map should be k:{1,...,m}->{0,1}, not k:{1,...,n}->{0,1}; n=2^m is the number of conjunctions.
  4. [Section 4, after Theorem 4.9] The sentence 'whence the induced presentation on M^{[0,1)} is computable by Corollary 3.3' should refer to Corollary 3.4 (decidable presentation implies computable induced presentation), and the assertion that ω-categoricity alone supplies a decidable presentation needs a proof or reference.
  5. [Section 2.1, simple functions] The definition of a simple function should specify the value on the complement of ∪I_i; otherwise the displayed special points of the induced presentation need not be total M-valued random variables.
  6. [Section 3, after Theorem 3.5] The phrase 'second half of the preceding corollary' should be 'second half of the preceding theorem'.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity; the central results are independently derived, with only minor reliance on the authors' prior general-purpose lemmas and one repairable proof gap.

full rationale

The derivation chain is largely self-contained. In Theorem 3.5, the converse direction runs through Proposition 2.10, which invokes the computable categoricity of B([0,1)) established in Theorem 4.4; that theorem is proved by a direct back-and-forth construction rather than imported from a self-citation. The one place where the authors' prior work is used is Fact 4.3, quoted from [6]: 'every nonempty c.e. closed subset X of N# contains a computable point.' This is a parameter-free general lemma whose stated assumptions do not include any target conclusion of this paper, so by the review rules it counts as independent support rather than a circular premise. Similarly, the citation to [7] concerns the standard equivalence of computable maps and is not load-bearing. Section 5's effective quantifier-elimination is derived from Keisler's classical randomization facts (Fact 5.10) and from an independently established effective quantifier-elimination result for atomless probability algebras (Theorem 5.7); there is no fitted parameter renamed as a prediction and no equation that reduces to its own input by construction. The only flagged item is the unproved line in Theorem 4.4, 'By countable saturation, p is realized in B([0,1)).' For the finite types that actually arise in the back-and-forth, the needed realization can be supplied by an elementary argument, so this is a repairable proof gap, not a circular step. No self-citation chain forces the paper's conclusions, and no uniqueness theorem is imported from the authors to forbid alternatives.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

No free parameters are fitted to data. The paper introduces no new postulated entities; its new definitions (awareness, effective recognizability, effective QE) are properties, not entities.

assumptions (6)
  • standard math Facts from continuous logic, including the framework of metric structures and their presentations (reference [3]).
    Used throughout for definitions of presentations, generated points, restricted formulas, and types.
  • standard math Keisler randomization facts, including density of witnesses for existential events (Fact 2.1).
    Imported from prior literature [1,4,9]; underpins Proposition 3.1 and the rounding arguments.
  • standard math Quantifier elimination for atomless probability algebras (reference [3, Proposition 16.6]).
    Used in Section 4 to isolate types over finite tuples in B([0,1)).
  • domain assumption Countable saturation of the atomless probability algebra.
    Invoked in Theorem 4.4 without proof; needed to realize types during the back-and-forth.
  • domain assumption Effective ω-categoricity (Definition 4.7): an algorithm returns isolating formulae for finitely many (n+1)-types.
    Assumed for Theorem 4.9; not automatic for every ω-categorical structure.
  • domain assumption Awareness of the presentation (Definition 2.4): M is a c.e. closed subset.
    Core hypothesis of the main equivalence; the paper leaves open whether it can be dropped.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Computable presentations of randomizations." pith.science (2026). https://pith.science/paper/T4XBP2ZF

@misc{pith2026250606187,
  author       = {Pith},
  title        = {Pith review of: Computable presentations of randomizations},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/T4XBP2ZF}},
  note         = {Machine review of arXiv:2506.06187}
}
abstract

We initiate the effective metric structure theory of Keisler randomizations. We show that a classical countable structure $\mathcal{M}$ has a decidable presentation if and only if its Borel randomization $\mathcal{M}^{[0,1)}$ has a computable presentation for which the constant functions are uniformly computable points. We determine a sufficient condition for which the uniform computability of the constant functions can be dropped. We show that when $\mathcal{M}$ is effectively $\omega$-categorical, then $\mathcal{M}^{[0,1)}$ is computably categorical, that is, has a unique computable presentation up to computable isomorphism. A special case of this result is that the unique separable atomless probability algebra is computably categorical. Finally, we show that all randomizations admit effective quantifier elimination.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

11 extracted references · 10 canonical work pages

  1. [1]

    Ben Yaacov, On theories of random variables, Israel J

    I. Ben Yaacov, On theories of random variables, Israel J. Math. 194 (2013), 957-1012

  2. [2]

    Continuous and random Vapnik-Chervonenkis classes, Israel Journal of Mathematics 173 (2009), 309-333

  3. [3]

    Ben Yaacov, A

    I. Ben Yaacov, A. Berenstein, C. W. Henson, A. Usvyatsov, Model theory for metric structures, London Mathematical Society Lecture Notes Series, Volume 2, (2008), 315-427

  4. [4]

    Ben Yaacov and H.J

    I. Ben Yaacov and H.J. Keisler, Randomizations of models as metric structures, Confluentes Mathematici 1 (2009), 197-223

  5. [5]

    Clanin, T

    J. Clanin, T. McNicholl, and D. Stull, Analytic computable structure theory and L^p spaces, Fundamenta Mathematicae 244 (2019), 255-285

  6. [6]

    Eagle, I

    C. Eagle, I. Goldbring, T. McNicholl, and R. Miller, Computable K-theory for C^* -algebras: UHF algebras , preprint. arXiv 2501.08526

  7. [7]

    Franklin, I

    J. Franklin, I. Goldbring, and T. McNicholl, Effective metric structure theory, manuscript in preparation

  8. [8]

    Goldbring and B

    I. Goldbring and B. Hart, The universal theory of the hyperfinite II _1 factor is not computable, Bulletin of Symbolic Logic 30 (2024), 181-198

Show all 11 references
  1. [9]

    Keisler, Randomizing a model, Advances in Mathematics 143 (1999), 124-158

    H.J. Keisler, Randomizing a model, Advances in Mathematics 143 (1999), 124-158

  2. [10]

    , Randomizations of scattered sentences, in Beyond First Order Model Theory (edited by Jose Iovino) 189-218, CRC Press

  3. [11]

    Andrews, and H.J

    U. Andrews, and H.J. Keisler, Separable models of randomizations, The Journal of Symbolic Logic, 80(4) (2015), 1149-1181

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.