Almost sure OTM-realizability

Merlin Carl

arxiv: 2403.10280 · v1 · pith:BH2L5ZOAnew · submitted 2024-03-15 · 🧮 math.LO

Almost sure OTM-realizability

Merlin Carl This is my paper

Pith reviewed 2026-05-24 03:53 UTC · model grok-4.3

classification 🧮 math.LO

keywords almost sure realizabilityordinal Turing machinesOTMintuitionistic logicKripke-Platek set theoryrealizability

0 comments

The pith

Almost sure realizability for parameter-free OTMs differs from plain realizability, while still closing under intuitionistic logic and realizing KP set theory.

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

The paper defines almost sure OTM-realizability by merging earlier approaches and shows that this version is not equivalent to ordinary realizability in the OTM setting. In the classical case the two notions coincide, but here they come apart. The new notion nevertheless remains closed under the rules of intuitionistic predicate logic and still realizes all axioms of Kripke-Platek set theory. A sympathetic reader would therefore see a strictly finer realizability relation that keeps the logical and set-theoretic properties already known for ordinary OTM-realizability.

Core claim

Almost sure realizability with parameter-free ordinal Turing machines is strictly different from plain OTM-realizability, in contrast to the classical situation, yet it is still closed under intuitionistic predicate logic and realizes Kripke-Platek set theory.

What carries the argument

Almost sure realizability defined via parameter-free ordinal Turing machines, obtained by combining the approaches of prior works.

If this is right

The distinction allows statements to be classified more finely than ordinary OTM-realizability permits.
All theorems of intuitionistic predicate logic remain realizable under the almost sure notion.
Every axiom of Kripke-Platek set theory continues to be realizable.
Results previously proved for plain OTM-realizability that rely only on the preserved closure properties carry over directly.

Where Pith is reading between the lines

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

The separation may let researchers isolate computability phenomena that ordinary realizability collapses.
One could test whether the same separation appears for other machine models or for realizability over different base theories.
If the distinction survives further extensions, it could supply a new tool for separating constructive and classical consequences inside set theory.

Load-bearing premise

The merged definition from earlier works produces a single coherent notion that separates almost sure from plain realizability while keeping the listed closure properties intact.

What would settle it

An explicit formula that is almost surely realizable but not plainly realizable, or a proof that the two notions coincide after all, or a failure of closure under intuitionistic logic or of KP-realizability under the new definition.

read the original abstract

Combining the approaches made in works with Galeotti and Passmann, we define and study a notion of "almost sure" realizability with parameter-free ordinal Turing machines (OTMs). In particular, we show that, in contrast to the classical case, almost sure realizability differs from plain realizability, while closure under intuitionistic predicate logic and realizability of Kripke-Platek set theory continue to hold.

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 defines almost sure OTM-realizability and shows it separates from plain realizability in the parameter-free OTM case while preserving closure under intuitionistic logic and KP-realizability.

read the letter

The key point is that almost sure realizability for parameter-free OTMs differs from plain realizability, unlike the classical case, while closure under intuitionistic predicate logic and realizability of KP set theory still hold. Carl builds this by combining prior techniques from the Galeotti and Passmann papers into a single definition and then checks the separation and preservation properties directly on it. That separation is the actual new piece; the preservation results serve as a sanity check that the new notion behaves as expected for the field. The work is straightforward in its execution and stays within the bounds of what the abstract promises without internal contradictions or unsupported leaps. The main limitation is scope. This stays inside ordinal computability and realizability, so it will mainly interest people already tracking OTM variants rather than a wider logic audience. No broader applications are claimed, which keeps the claims proportionate. The citation pattern looks clean, drawing on the relevant earlier results without circularity. Readers working on realizability interpretations or ordinal machines would find the distinction useful for seeing how the parameter-free setting changes the picture. The paper shows clear engagement with the literature and honest handling of the new definition. It deserves peer review so the proofs can be checked in detail.

Referee Report

0 major / 1 minor

Summary. The paper combines prior approaches with Galeotti and Passmann to define almost sure realizability for parameter-free ordinal Turing machines (OTMs). It claims that, unlike the classical case, this notion differs from plain realizability, while remaining closed under intuitionistic predicate logic and realizing Kripke-Platek set theory.

Significance. If the results hold, the distinction between almost sure and plain realizability in the OTM setting (absent classically) offers a new perspective on how parameter-freeness interacts with probabilistic or measure-theoretic notions of realizability. Preservation of the closure and KP-realizability properties indicates the definition is robust enough to support standard applications in constructive set theory.

minor comments (1)

The abstract refers to 'works with Galeotti and Passmann' without explicit citations; the introduction should list the specific prior papers being combined.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their summary of the manuscript and their assessment of its potential significance. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines a new notion of almost sure OTM-realizability by combining prior techniques from works with Galeotti and Passmann, then proves that this notion differs from plain realizability while retaining closure under intuitionistic predicate logic and realizability of KP set theory. These are direct consequences of the explicit construction and standard logical verification; no derivation step reduces by construction to its inputs, no fitted parameters are relabeled as predictions, and self-citations serve only as background for the combined definition rather than as load-bearing justification for the central distinctions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Only the abstract is available; no specific free parameters, ad-hoc axioms, or invented entities are identifiable from the given text. The work operates within standard frameworks of ordinal computability and set theory.

axioms (1)

standard math Standard background results on ordinal Turing machines and realizability from prior literature
The paper combines approaches from cited works without introducing new foundational assumptions visible in the abstract.

pith-pipeline@v0.9.0 · 5571 in / 1222 out tokens · 46720 ms · 2026-05-24T03:53:27.345919+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

44 extracted references · 44 canonical work pages

[1]

J. Barwise. Admissible Sets and Structures. Perspective s in Logic. Cambridge Uni- versity Press. (2017) 10.1017/9781316717196

work page doi:10.1017/9781316717196 2017
[2]

Bogachev

V. Bogachev. Measure Theory. Volume 1. Physica-Verlag (2 007)

work page
[3]

M. Carl. Ordinal Computability. An Introduction to Inﬁni tary Machines. De Gruyter (2019)

work page 2019
[4]

M. Carl. A Note on OTM-Realizability and Constructive Set Theories. Preprint. arXiv:1903.08945 (2019)

work page arXiv 1903
[5]

M. Carl, P. Schlicht. Inﬁnite Computations with Random Or acles. Notre Dame Journal of Formal Logic, 58(2) (2017)

work page 2017
[6]

Downey, D

R. Downey, D. Hirschfeldt. Algorithmic Randomness and Co mplexity. Springer (2010)

work page 2010
[7]

M. Carl, L. Galeotti, R. Passmann. Realisability for Inﬁn itary Intuitionistic Set Theory. Annals of Pure and Applied Logic, 174(6) (2023)

work page 2023
[8]

M. Carl, L. Galeotti, R. Passmann. Randomizing Realizabi lity. In: L. De Mol et al. (eds) Connecting with Computability. CiE 2021. Lecture Not es in Computer Science, 12813. Springer, Cham. 10.1007/978-3-030-80049-9_8

work page doi:10.1007/978-3-030-80049-9_8 2021
[9]

W. Hodges. On the Eﬀectivity of some Field Constructions. Proceedings of the London Mathematical Society, s3–32(1) (1976)

work page 1976
[10]

Iemhoﬀ, R

R. Iemhoﬀ, R. Passmann. Logics of intuitionistic Kripke -Platek set theory. Annals of Pure and Applied Logic, 172(10) (2021)

work page 2021
[11]

P. Koepke. Turing Computations on Ordinals. Bulletin of Symbolic Logic 11(3) (2005) https://doi.org/10.2178/bsl/1122038993

work page doi:10.2178/bsl/1122038993 2005
[12]

Lubarsky

B. Lubarsky. IKP and friends. Journal of Symbolic Logic 6 7(4) (2002) 10.2178/jsl/1190150286

work page doi:10.2178/jsl/1190150286 2002
[13]

Moschovakis

J. Moschovakis. Intuitionistic Logic. In: E. Zalta, U. Nodelman (eds.). The Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/archives/sum2023/entries/logic-intuitionistic/ (last accessed 05.02.2024) (2023)

work page 2024
[14]

Martin, J

D. Martin, J. Steel. A Proof of Projective Determinacy. J ournal of the American Mathematical Society, vol. 2(1). (1989)

work page 1989
[15]

M. Rathjen. Choice principles in constructive and class ical set theories. In: Chatzi- dakis Z, Koepke P, Pohlers W, eds. Logic Colloquium ’02. Lect ure Notes in Logic. Cambridge University Press. (2006)

work page 2006
[16]

N. Wontner. Views from a Peak. Generalisations and descr iptive set theory. ILLC Dissertation Series DS-2023-NN (2023) Almost sure OTM-realizability 13 6 Appendix: Proofs We give the proofs of some lemmas and theorems that had to be omitt ed in the paper due to the page limit for the sake of the referees. Lemma 4: Lemma 22. (Cf. [7], Lemma 21-23) There is...

work page 2023
[17]

ϕ is plainly OTM-realizable

work page
[18]

ϕ is as-OTM-realizable

work page
[19]

ϕ is true. Proof. This is trivial for the case that ϕ itself is ∆0; the details are analogous to those in the proof of [7], Lemma 23. We assume from now on that the s tatement is proved for this case. In the general case, the realizer r will work as follows: Given a real number x coding a set a, use the OTM-program PL from [3], Lemma 3 .5.313 that, on inp...

work page
[20]

Then µ( ˜⨂n i=0fi) = 1

More generally, let n ∈ ω, fi : [0 , 1]i → P([0, 1]) for i ∈ { 0, ..., n} such that the following holds for all k ≤ n − 1: There is a Ok ⊆ [0, 1]k with µ(Ok) = 1 and µ(fk(x0, ..., xk− 1)) = 1 for all (x0, ..., xk− 1) ∈ O k. Then µ( ˜⨂n i=0fi) = 1 . Proof. 1. Let χA be the characteristic function of A; by assumption, χA is measurable. Deﬁne f : [0, 1] → { ...

work page
[21]

For n = 2, this is part (1)

This now follows inductively with the help of Lemma 15. For n = 2, this is part (1). Now suppose that the statement is true for n. Encode ˜⨂n i=0fi as a subset of [0 , 1] as described above. For each x ∈ [0, 1], let Sx := {(x1, ..., xn) : (x, x1, ..., xn) ∈ ˜⨂n i=0fi}. By the inductive assumption, µ(Sx) = 1 for all x ∈ f0. Deﬁne, for each x ∈ [0, 1], ˜Sx ...

work page
[22]

are sound for as-OTM-realizability. The proof of this statement is split into the following two sublemmas, w hich state that soundness holds for the deduction rules and for the ax iom (schemes) of the mentioned calculus, respectively. The arguments are similar to t hose given in the (unpublished) appendix to [8], which will appear in forthcoming wo rk wit...

work page
[23]

If a has no free occurences in ϕ, then {ϕ → ψ} ⊢ ϕ → ∀ aψ(a)

work page
[24]

If a has no free occurences in ψ, then {ϕ(a) → ψ} ⊢ ∃ aϕ(a) → ψ Proof. 1. Let as-OTM-realizers rϕ, rϕ→ ψ for ϕ and ϕ → ψ be given. The as- OTM-realizer computed from rϕ and rϕ→ ψ is the program Q that, in the oracle x, does the following: Let a relevant input ξ for ψ be given. Decompose x into x = x0 ⊕ x1. Compute rx0 := rx0 ϕ→ ψ(rϕ). Then compute rx1 x0 ...

work page
[25]

Otherwise, by deﬁnition of as-OTM-realizability for formulas with free variables, an as-OTM- realizer for ϕ → ψ(a) is one for ∀a(ϕ → ψ(a))

If x does not occur freely in ψ either, this is trivial. Otherwise, by deﬁnition of as-OTM-realizability for formulas with free variables, an as-OTM- realizer for ϕ → ψ(a) is one for ∀a(ϕ → ψ(a)). Let such an as-OTM-realizer rϕ→ ψ(a) be given. Our as-OTM-realizer for ϕ → ∀ aψ(x) will work in the following way: Given an as-OTM-realizer rϕ for ϕ, a relevant...

work page
[26]

Moreover, let x ⊆ ω be a real number

Let as-OTM-realizers r∀ ⊩OTM as (ϕ(a) → ψ) and r∃ ⊩OTM as ∃aϕ(a) be given. Moreover, let x ⊆ ω be a real number. Finally, let ξ be a relevant input for ψ. Our as-OTM-realizer Q is an as-OTM-program that, given this data, decom- poses x into x = ⨁3 i=0 xi and then computes (( rx0 ∀ (rx1 ∃ (1)))x2 (rx1 ∃ (0)))x3 (ξ). If x is such that x1 ∈ succr∃ , we will ...

work page
[27]

(ϕ → ψ) → ((ϕ → (ψ → χ)) → (ϕ → χ))

work page
[28]

(ϕ ∧ ψ) → ϕ and (ϕ ∧ ψ) → ψ

work page
[29]

ϕ → (ϕ ∨ ψ) and ψ → (ϕ ∨ ψ)

work page
[30]

(ϕ → χ) → ((ψ → χ) → ((ϕ ∨ ψ) → χ)) 16 Merlin Carl

work page
[31]

(ϕ → ψ) → ((ϕ → ¬ ψ) → ¬ ϕ)

work page
[32]

unrandomized

ϕ(t) → ∃ xϕ(x) Proof. For the most part, the proofs are obvious and the details given in [7], section 4.1, for “unrandomized” OTMs go through. We thus focus o n the cases that are more involved or involve the oracle in some relevant way

work page
[33]

We need to compute an as-OTM-realizer r for ((ϕ → (ψ → χ)) → (ϕ → χ))

Let rϕ→ ψ ⊩OTM as ϕ → ψ. We need to compute an as-OTM-realizer r for ((ϕ → (ψ → χ)) → (ϕ → χ)). r will, on input rϕ→ (ψ→ ξ) ⊩OTM as ϕ → (ψ → χ), output the code of an OTM-program P that does the following: Given a real number x and an as-OTM-realizer rϕ ⊩OTM as ϕ, we let x =: x0 ⊕ x1. Then successively compute r0,x := rx0 ϕ→ ψ(rϕ), r1,x := rx0 ϕ→ (ψ→ χ)(r...

work page
[34]

Let rϕ→ χ ⊩OTM as ϕ → χ be given. Our procedure will map this to the OTM- program r which works as follows: Given rψ→ χ ⊩OTM as ψ → χ, output the OTM-program r′ which has the following function: Given rϕ∨ ψ ⊩OTM as ϕ ∨ ψ, along with x ⊆ ω, ﬁrst compute j := rx0 ϕ∨ χ(0). Then one of the following cases occurs: (a) If j = 0, compute rx1 ϕ→ χ(rx0 ϕ∨ ψ(1)) an...

work page
[35]

Let rϕ→ ψ ⊩OTM as ϕ → ψ

Recall that we interpret ¬ ϕ as ϕ → (1 = 0). Let rϕ→ ψ ⊩OTM as ϕ → ψ. We will compute on this input the OTM-program r that works as follows: Given rϕ→¬ ψ ⊩OTM as , rϕ ⊩OTM as ϕ and x ⊆ ω, we proceed as follows: Decompose x =: x0 ⊕ x1. Then compute r0 := rx0 ϕ→ ψ(rϕ) and r1 := rx0 ϕ→¬ ψ(rϕ). Then return rx1 1 (r0). If x is such that x0 ∈ succrϕ rϕ→ψ ∩ succ...

work page
[36]

Let r¬ ϕ be an as-OTM-realizer of ¬ ϕ, i.e., of ϕ → (1 = 0). If there was an as-OTM-realizer r for ϕ, then, taking x ∈ succr r¬ϕ , we would have that rx ¬ ϕ(rϕ) ⊢ OTM as (1 = 0), which, by deﬁnition of as-OTM-realizability for Almost sure OTM-realizability 17 atomic formulas, cannot be. It follows that ϕ has no as-OTM-realizers. Thus, we can output the OT...

work page
[37]

Call this procedure P ; then succ t P = succ t r∀ ∈ B

Given r∀ ⊩OTM as ∀aϕ(a), a set t ∈ Hω1 and a real number x, we output rx ∀ (t). Call this procedure P ; then succ t P = succ t r∀ ∈ B

work page
[38]

Lemma 28

Given an as-OTM-realizer rϕ of ϕ(t), return the program that, on input 0, returns rϕ while on input 1, it returns t (recall that, by clause (4) in the deﬁnition of as-OTM-realizers, the parameters used in the antece dent of an implication are passed on to the program realizing the succedent, so that t is indeed available). Lemma 28. 1. The axioms of exten...

work page
[39]

The ∆0-separation scheme is as-OTM-realizable

work page
[40]

The (full) collection scheme is as-OTM-realizable

work page
[41]

The induction scheme is OTM-realizable. Proof. 1. Trivial

work page
[42]

Let a set X ∈ Hω1 be given, along with a ∆0-formula ϕ and a real number x.14 To compute Xϕ := {a ∈ X : ϕ(a)}, we can ignore x and use the fact that truth of ∆0-formulas is easily seen to be decidable on an OTM; computing an as-OTM-realizer for a true ∆0-statement ϕ (uniformly in ϕ) then works as in [8], Theorem 25

work page
[43]

We want to realize the following statement: ∀X((∀x ∈ X∃yϕ(x, y)) → ∃ Y ∀x ∈ X∃y ∈ Y ϕ(x, y))

Let ϕ(x, y) be ∆0. We want to realize the following statement: ∀X((∀x ∈ X∃yϕ(x, y)) → ∃ Y ∀x ∈ X∃y ∈ Y ϕ(x, y)). So let a (code for a) set X be given. Moreover, suppose that r ⊩as-OTM ∀x ∈ X∃yϕ(x, y). For each x ∈ X, there is a set Ox ∈ B such that ϕ(x, ry (x)) for all y ∈ O x. Let O := ⋂ x∈ X Ox. Since X is countable, we have µ(O) = 1. So, relative to th...

work page
[44]

However, showing that the ocuring success sets h ave measure 1 requires some care; we therefore give the proof in deta ils

This leaves us with induction; our argument will be similar to the one f or Theorem 43 in [8]. However, showing that the ocuring success sets h ave measure 1 requires some care; we therefore give the proof in deta ils. We need to provide an OTM-eﬀective method that, given an ∈ -formula ϕ, computes an as-OTM-realizer for Indϕ := ∀a((∀b ∈ aϕ(b)) → ϕ(a)) → ∀...

work page

[1] [1]

J. Barwise. Admissible Sets and Structures. Perspective s in Logic. Cambridge Uni- versity Press. (2017) 10.1017/9781316717196

work page doi:10.1017/9781316717196 2017

[2] [2]

Bogachev

V. Bogachev. Measure Theory. Volume 1. Physica-Verlag (2 007)

work page

[3] [3]

M. Carl. Ordinal Computability. An Introduction to Inﬁni tary Machines. De Gruyter (2019)

work page 2019

[4] [4]

M. Carl. A Note on OTM-Realizability and Constructive Set Theories. Preprint. arXiv:1903.08945 (2019)

work page arXiv 1903

[5] [5]

M. Carl, P. Schlicht. Inﬁnite Computations with Random Or acles. Notre Dame Journal of Formal Logic, 58(2) (2017)

work page 2017

[6] [6]

Downey, D

R. Downey, D. Hirschfeldt. Algorithmic Randomness and Co mplexity. Springer (2010)

work page 2010

[7] [7]

M. Carl, L. Galeotti, R. Passmann. Realisability for Inﬁn itary Intuitionistic Set Theory. Annals of Pure and Applied Logic, 174(6) (2023)

work page 2023

[8] [8]

M. Carl, L. Galeotti, R. Passmann. Randomizing Realizabi lity. In: L. De Mol et al. (eds) Connecting with Computability. CiE 2021. Lecture Not es in Computer Science, 12813. Springer, Cham. 10.1007/978-3-030-80049-9_8

work page doi:10.1007/978-3-030-80049-9_8 2021

[9] [9]

W. Hodges. On the Eﬀectivity of some Field Constructions. Proceedings of the London Mathematical Society, s3–32(1) (1976)

work page 1976

[10] [10]

Iemhoﬀ, R

R. Iemhoﬀ, R. Passmann. Logics of intuitionistic Kripke -Platek set theory. Annals of Pure and Applied Logic, 172(10) (2021)

work page 2021

[11] [11]

P. Koepke. Turing Computations on Ordinals. Bulletin of Symbolic Logic 11(3) (2005) https://doi.org/10.2178/bsl/1122038993

work page doi:10.2178/bsl/1122038993 2005

[12] [12]

Lubarsky

B. Lubarsky. IKP and friends. Journal of Symbolic Logic 6 7(4) (2002) 10.2178/jsl/1190150286

work page doi:10.2178/jsl/1190150286 2002

[13] [13]

Moschovakis

J. Moschovakis. Intuitionistic Logic. In: E. Zalta, U. Nodelman (eds.). The Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/archives/sum2023/entries/logic-intuitionistic/ (last accessed 05.02.2024) (2023)

work page 2024

[14] [14]

Martin, J

D. Martin, J. Steel. A Proof of Projective Determinacy. J ournal of the American Mathematical Society, vol. 2(1). (1989)

work page 1989

[15] [15]

M. Rathjen. Choice principles in constructive and class ical set theories. In: Chatzi- dakis Z, Koepke P, Pohlers W, eds. Logic Colloquium ’02. Lect ure Notes in Logic. Cambridge University Press. (2006)

work page 2006

[16] [16]

N. Wontner. Views from a Peak. Generalisations and descr iptive set theory. ILLC Dissertation Series DS-2023-NN (2023) Almost sure OTM-realizability 13 6 Appendix: Proofs We give the proofs of some lemmas and theorems that had to be omitt ed in the paper due to the page limit for the sake of the referees. Lemma 4: Lemma 22. (Cf. [7], Lemma 21-23) There is...

work page 2023

[17] [17]

ϕ is plainly OTM-realizable

work page

[18] [18]

ϕ is as-OTM-realizable

work page

[19] [19]

ϕ is true. Proof. This is trivial for the case that ϕ itself is ∆0; the details are analogous to those in the proof of [7], Lemma 23. We assume from now on that the s tatement is proved for this case. In the general case, the realizer r will work as follows: Given a real number x coding a set a, use the OTM-program PL from [3], Lemma 3 .5.313 that, on inp...

work page

[20] [20]

Then µ( ˜⨂n i=0fi) = 1

More generally, let n ∈ ω, fi : [0 , 1]i → P([0, 1]) for i ∈ { 0, ..., n} such that the following holds for all k ≤ n − 1: There is a Ok ⊆ [0, 1]k with µ(Ok) = 1 and µ(fk(x0, ..., xk− 1)) = 1 for all (x0, ..., xk− 1) ∈ O k. Then µ( ˜⨂n i=0fi) = 1 . Proof. 1. Let χA be the characteristic function of A; by assumption, χA is measurable. Deﬁne f : [0, 1] → { ...

work page

[21] [21]

For n = 2, this is part (1)

This now follows inductively with the help of Lemma 15. For n = 2, this is part (1). Now suppose that the statement is true for n. Encode ˜⨂n i=0fi as a subset of [0 , 1] as described above. For each x ∈ [0, 1], let Sx := {(x1, ..., xn) : (x, x1, ..., xn) ∈ ˜⨂n i=0fi}. By the inductive assumption, µ(Sx) = 1 for all x ∈ f0. Deﬁne, for each x ∈ [0, 1], ˜Sx ...

work page

[22] [22]

are sound for as-OTM-realizability. The proof of this statement is split into the following two sublemmas, w hich state that soundness holds for the deduction rules and for the ax iom (schemes) of the mentioned calculus, respectively. The arguments are similar to t hose given in the (unpublished) appendix to [8], which will appear in forthcoming wo rk wit...

work page

[23] [23]

If a has no free occurences in ϕ, then {ϕ → ψ} ⊢ ϕ → ∀ aψ(a)

work page

[24] [24]

If a has no free occurences in ψ, then {ϕ(a) → ψ} ⊢ ∃ aϕ(a) → ψ Proof. 1. Let as-OTM-realizers rϕ, rϕ→ ψ for ϕ and ϕ → ψ be given. The as- OTM-realizer computed from rϕ and rϕ→ ψ is the program Q that, in the oracle x, does the following: Let a relevant input ξ for ψ be given. Decompose x into x = x0 ⊕ x1. Compute rx0 := rx0 ϕ→ ψ(rϕ). Then compute rx1 x0 ...

work page

[25] [25]

Otherwise, by deﬁnition of as-OTM-realizability for formulas with free variables, an as-OTM- realizer for ϕ → ψ(a) is one for ∀a(ϕ → ψ(a))

If x does not occur freely in ψ either, this is trivial. Otherwise, by deﬁnition of as-OTM-realizability for formulas with free variables, an as-OTM- realizer for ϕ → ψ(a) is one for ∀a(ϕ → ψ(a)). Let such an as-OTM-realizer rϕ→ ψ(a) be given. Our as-OTM-realizer for ϕ → ∀ aψ(x) will work in the following way: Given an as-OTM-realizer rϕ for ϕ, a relevant...

work page

[26] [26]

Moreover, let x ⊆ ω be a real number

Let as-OTM-realizers r∀ ⊩OTM as (ϕ(a) → ψ) and r∃ ⊩OTM as ∃aϕ(a) be given. Moreover, let x ⊆ ω be a real number. Finally, let ξ be a relevant input for ψ. Our as-OTM-realizer Q is an as-OTM-program that, given this data, decom- poses x into x = ⨁3 i=0 xi and then computes (( rx0 ∀ (rx1 ∃ (1)))x2 (rx1 ∃ (0)))x3 (ξ). If x is such that x1 ∈ succr∃ , we will ...

work page

[27] [27]

(ϕ → ψ) → ((ϕ → (ψ → χ)) → (ϕ → χ))

work page

[28] [28]

(ϕ ∧ ψ) → ϕ and (ϕ ∧ ψ) → ψ

work page

[29] [29]

ϕ → (ϕ ∨ ψ) and ψ → (ϕ ∨ ψ)

work page

[30] [30]

(ϕ → χ) → ((ψ → χ) → ((ϕ ∨ ψ) → χ)) 16 Merlin Carl

work page

[31] [31]

(ϕ → ψ) → ((ϕ → ¬ ψ) → ¬ ϕ)

work page

[32] [32]

unrandomized

ϕ(t) → ∃ xϕ(x) Proof. For the most part, the proofs are obvious and the details given in [7], section 4.1, for “unrandomized” OTMs go through. We thus focus o n the cases that are more involved or involve the oracle in some relevant way

work page

[33] [33]

We need to compute an as-OTM-realizer r for ((ϕ → (ψ → χ)) → (ϕ → χ))

Let rϕ→ ψ ⊩OTM as ϕ → ψ. We need to compute an as-OTM-realizer r for ((ϕ → (ψ → χ)) → (ϕ → χ)). r will, on input rϕ→ (ψ→ ξ) ⊩OTM as ϕ → (ψ → χ), output the code of an OTM-program P that does the following: Given a real number x and an as-OTM-realizer rϕ ⊩OTM as ϕ, we let x =: x0 ⊕ x1. Then successively compute r0,x := rx0 ϕ→ ψ(rϕ), r1,x := rx0 ϕ→ (ψ→ χ)(r...

work page

[34] [34]

Let rϕ→ χ ⊩OTM as ϕ → χ be given. Our procedure will map this to the OTM- program r which works as follows: Given rψ→ χ ⊩OTM as ψ → χ, output the OTM-program r′ which has the following function: Given rϕ∨ ψ ⊩OTM as ϕ ∨ ψ, along with x ⊆ ω, ﬁrst compute j := rx0 ϕ∨ χ(0). Then one of the following cases occurs: (a) If j = 0, compute rx1 ϕ→ χ(rx0 ϕ∨ ψ(1)) an...

work page

[35] [35]

Let rϕ→ ψ ⊩OTM as ϕ → ψ

Recall that we interpret ¬ ϕ as ϕ → (1 = 0). Let rϕ→ ψ ⊩OTM as ϕ → ψ. We will compute on this input the OTM-program r that works as follows: Given rϕ→¬ ψ ⊩OTM as , rϕ ⊩OTM as ϕ and x ⊆ ω, we proceed as follows: Decompose x =: x0 ⊕ x1. Then compute r0 := rx0 ϕ→ ψ(rϕ) and r1 := rx0 ϕ→¬ ψ(rϕ). Then return rx1 1 (r0). If x is such that x0 ∈ succrϕ rϕ→ψ ∩ succ...

work page

[36] [36]

Let r¬ ϕ be an as-OTM-realizer of ¬ ϕ, i.e., of ϕ → (1 = 0). If there was an as-OTM-realizer r for ϕ, then, taking x ∈ succr r¬ϕ , we would have that rx ¬ ϕ(rϕ) ⊢ OTM as (1 = 0), which, by deﬁnition of as-OTM-realizability for Almost sure OTM-realizability 17 atomic formulas, cannot be. It follows that ϕ has no as-OTM-realizers. Thus, we can output the OT...

work page

[37] [37]

Call this procedure P ; then succ t P = succ t r∀ ∈ B

Given r∀ ⊩OTM as ∀aϕ(a), a set t ∈ Hω1 and a real number x, we output rx ∀ (t). Call this procedure P ; then succ t P = succ t r∀ ∈ B

work page

[38] [38]

Lemma 28

Given an as-OTM-realizer rϕ of ϕ(t), return the program that, on input 0, returns rϕ while on input 1, it returns t (recall that, by clause (4) in the deﬁnition of as-OTM-realizers, the parameters used in the antece dent of an implication are passed on to the program realizing the succedent, so that t is indeed available). Lemma 28. 1. The axioms of exten...

work page

[39] [39]

The ∆0-separation scheme is as-OTM-realizable

work page

[40] [40]

The (full) collection scheme is as-OTM-realizable

work page

[41] [41]

The induction scheme is OTM-realizable. Proof. 1. Trivial

work page

[42] [42]

Let a set X ∈ Hω1 be given, along with a ∆0-formula ϕ and a real number x.14 To compute Xϕ := {a ∈ X : ϕ(a)}, we can ignore x and use the fact that truth of ∆0-formulas is easily seen to be decidable on an OTM; computing an as-OTM-realizer for a true ∆0-statement ϕ (uniformly in ϕ) then works as in [8], Theorem 25

work page

[43] [43]

We want to realize the following statement: ∀X((∀x ∈ X∃yϕ(x, y)) → ∃ Y ∀x ∈ X∃y ∈ Y ϕ(x, y))

Let ϕ(x, y) be ∆0. We want to realize the following statement: ∀X((∀x ∈ X∃yϕ(x, y)) → ∃ Y ∀x ∈ X∃y ∈ Y ϕ(x, y)). So let a (code for a) set X be given. Moreover, suppose that r ⊩as-OTM ∀x ∈ X∃yϕ(x, y). For each x ∈ X, there is a set Ox ∈ B such that ϕ(x, ry (x)) for all y ∈ O x. Let O := ⋂ x∈ X Ox. Since X is countable, we have µ(O) = 1. So, relative to th...

work page

[44] [44]

However, showing that the ocuring success sets h ave measure 1 requires some care; we therefore give the proof in deta ils

This leaves us with induction; our argument will be similar to the one f or Theorem 43 in [8]. However, showing that the ocuring success sets h ave measure 1 requires some care; we therefore give the proof in deta ils. We need to provide an OTM-eﬀective method that, given an ∈ -formula ϕ, computes an as-OTM-realizer for Indϕ := ∀a((∀b ∈ aϕ(b)) → ϕ(a)) → ∀...

work page