de Jong, Kraus, Mohammadzadeh, and Nordvall Forsberg put an ordinal axis under decidability. One definition — α-decidability — subsumes decidable propositions, semidecidable propositions, ∀-of-semidecidable, and a hierarchy of quantifier alternations. The ordinal is the shape of the witness.
We read that axis as past-tense. The paper doesn't frame it that way, but the constructions below read as monotone accumulators over completed observations, which is the job the tropical semiring does on the left side of the zipper. Their Theorem 8.4 — that countable choice is not enough to collapse the ω² layer — is what we wanted from it: a separation result from a setting with no nets in it, sitting close to the claim in The Pflow Square that the past/future split is forced rather than chosen. Close to is as far as it goes. Nothing below turns the theorem into a statement about nets.
Paper: arXiv:2602.10844 — Generalized Decidability via Brouwer Trees, with a Cubical Agda formalization.
Prerequisites: Tropical Petri Nets for the max-plus vector x(k), and The Zipper Whose Hole Is a Universe for past, hole and future. Revised 2026-10-30; see What Changed, including which statements about the paper were not re-checked.
α-decidable P := ∃ y : Brw. (P ↔ α ≤ y)
Brw is the type of Brouwer ordinals. α is a fixed threshold. P is α-decidable when there exists a Brouwer ordinal y such that P holds iff y has grown past α.
| Class | Threshold |
|---|---|
P already holds |
ω·0 |
| decidable | ω·1 |
| semidecidable | ω·2 |
| Twin Prime (∀ of semidec) | ω² |
| ∃ of semidec (no choice) | ω·3 |
| ∃m. ∀n. P(n,m) upward-closed | ω²+ω |
All of these are instances of the same definition; the only thing that changes is α. Under countable choice the classes at ω·k with k ≥ 2 collapse onto semidecidable. The two below it stay below it, since decidable = semidecidable would be LPO. Nothing proves that the ω² layer, or anything above it, comes down to semidecidable the same way; the argument is below.
Brw is a quotient inductive-inductive type with three point constructors, zero, succ and limit (f : ℕ → Brw), where limit accepts only strictly increasing sequences, plus the path constructors that make it a quotient.
The strict-increase constraint is load-bearing. A Brouwer ordinal only takes a limit when strict progress has been witnessed, so limit f carries the function and evidence that each step advanced. As we read it, that evidence is what makes the construction usable constructively without choice.
The order α ≤ β on Brw is inductively defined and prelinear, not linear: in general we cannot prove α ≤ β ∨ β ≤ α without classical assumptions. One witness lines up one history. Two witnesses from independent histories need not be comparable in any way we can prove, which comes back in the concurrent gap below.
The paper gives a uniform procedure for building a Brouwer witness from an observation process. For a proposition P observed at stages n : ℕ:
Ψ(P) := limit(λn. Ψₙ(P) + n)
Each Ψₙ(P) summarizes everything observed about P through stage n. The + n guarantees strict increase even when observation stalls. The limit is the completed observation process.
Ψ(P) is a monotone accumulator: it grows as observations accumulate, never retracts, and ends in a limit of strict progress. An ordinal that grows with observation is what we mean by a past-tense object — the history compressed to its order type.
Theorem 8.4 is the payoff. Under countable choice, every finite-k α-decidable proposition (α = ω·k) is semidecidable. The obvious hope is that with enough choice you can flatten the quantifier-alternation layer at ω² the same way, and that can't be proved.
Collapsing ω²-decidable to semidecidable would prove MP ⇒ LPO. The step is short enough to give, and this is our reconstruction rather than the paper's text. Let P be semidecidable, P ↔ ∃n. f n = 1 for some f : ℕ → 2. Then ¬P ↔ ∀n. f n = 0 is a ∀ of decidables, so it sits at ω², so under the collapse ¬P is semidecidable too. That makes P ∨ ¬P semidecidable, and it is not-not-true in any case, so Markov's Principle gives P ∨ ¬P. For every f, that is the Limited Principle of Omniscience. Markov's Principle does not imply LPO constructively: Markov's own school of recursive mathematics has countable choice and MP and refutes LPO, which is why adding choice doesn't help. Classically the collapse is trivial, because everything is decidable. The obstruction is about what can be proved short of that.
So the ∀n. semidec(n) step — the jump from ω·2 to ω² — can't be absorbed into a single-pass observation process, even with choice, unless something classical beyond Markov's Principle comes with it.
Defining functions out of a QIIT like Brw by direct pattern-matching forces you to handle every path constructor, and for higher-dimensional paths the coherence burden explodes. The paper's construction of limMin : Brw × Brw → Brw hit over three dozen cases with 3D and 4D cube fills.
§9.1 replaces the direct construction with a relational one. Define a relation R : Brw × Brw × Brw → Type on point constructors only. Prove R is single-valued and total. Then Σ z. R x y z is contractible and the function extracts via the first projection. The path-constructor cases are discharged by the fact that R is a type family — it respects the paths. Single-valuedness plus totality extracts the function without touching any higher-dimensional fills.
The resemblance is to Bove and Capretta (Modelling general recursion in type theory): describe the computation inductively first and get the function out of that description afterward. They do it for partial recursive functions with a domain predicate; here it is a graph relation and unique choice on a higher inductive type, so "adapted" is our word. It should transfer to other functions out of a QIIT carrier — marking quotients, Chu-space equalities, forgetful functors between net categories — but we haven't tried it on any of those, and none of our net code is in Cubical Agda.
P ↔ α ≤ y reads as: P holds exactly when the accumulator has crossed the threshold. The accumulator grows under observation; the threshold is fixed. On this reading the future-tense claim — P will hold — is equivalent to a past-tense fact: y has grown past α.
That is close to the shape the zipper draws around execution state, where the marking is the hole between an accumulated past and a predicate recomputed on every step. The fit is loose at one point: a guard reads the marking, and the threshold test here reads the accumulator directly. The tense reading is ours. The paper says nothing about it.
We read the ordinal as how much past the proposition needs. Decidable propositions need a bounded past. Semidecidable propositions need an ω-bounded past. Twin Prime needs an ω²-bounded past because it quantifies ∀n over a semidecidable process — the outer universal forces completion of the inner ω-processes before committal. The hierarchy then measures how much history the witness has to compress rather than how long the proof is.
A timed event graph carries a max-plus vector x(k) over (ℝ ∪ {−∞}, max, +), one coordinate per transition, holding the k-th firing time of each — a vector past, as far as the left context is tropical at all, which The Pflow Square leaves argued rather than proved. Their framework carries y : Brw — a scalar past, one ordinal total.
Specialize to one coordinate: a single transition looping through one place, x(k+1) = a ⊗ x(k) = x(k) + a. For a > 0 that runs x(0) + k·a, a strictly increasing sequence indexed by ℕ, which is the kind of data limit accepts, and Ψₙ(P) + n has the same shape. The match stops at the sequence. ℝ is dense and its order is not well-founded, so nothing in it is order-isomorphic to Brw, and the run diverges with no limit in the carrier, so ω·2 and ω² have no value to land on. Whether Ψₙ of some proposition tracks the run of some net step by step is the question we'd want settled, and we haven't built either side of it.
The vector side does have something the scalar one lacks. Transitions that no place connects have −∞ between them in A, so their coordinates accumulate independently and x(k) splits along the net's components. Pointwise order on these vectors is partial — two of them can be incomparable. Brouwer ordinals are prelinear; these vectors are plainly partial.
Two independent firings in a Petri net can happen in either order without changing the final marking. A scalar accumulator has two ways to take that, and neither keeps them independent. It can count, which doesn't care about order and forgets which firings happened. Or it can use ordinal addition, which does see order — 1 + ω = ω but ω + 1 > ω — and then choosing the accumulator amounts to choosing a schedule.
A concurrent past needs an accumulator invariant under Mazurkiewicz equivalence of firing sequences that still records what fired. We expect Brouwer ordinals to be the wrong carrier, because one value can't hold two firings apart the way two incomparable coordinates can. We haven't proved that: Brw is only prelinear, so totality isn't the argument, and we haven't looked for an encoding that uses the gap. The candidates we'd try are Brouwer-indexed diagrams over a partial order — event structures, pomset-indexed limits, a Brouwer poset — and none of them is built.
The paper does not construct one. The vector side looks like the place to start, because the event-graph recursion defines firing times with no schedule in it. That covers event graphs only, and a general net with choice and shared places is not max-plus linear. We found no test of the invariance in pflow-tropical.
The ω² obstruction is a statement about constructive provability over one scalar carrier. If it says anything about the boundary between past and future in a net, the way to find out is to exhibit a net whose past needs that layer. We haven't, and until someone does the theorem is a rhyme with the zipper rather than support for it.
For readers of the April version (revised 2026-10-30). Nothing here was run; the statements about the paper itself — the threshold table, Ψ, §9.1, the count of cube fills, the theorem's number — were kept from April and not re-read against the paper in this revision.
T : Place → ℝ ∪ {∞} under min-plus. The blog's tropical past is max-plus over ℝ ∪ {−∞}, with one coordinate per transition, and the marking is the hole M, not the past.limit argument. We found no test behind the stronger claim.MP ⇒ LPO. That derivation is ours.k classes collapse together" is true for k ≥ 2. Decidable stays below semidecidable.sup, which is why they can be classically well-ordered" didn't follow.Related: The Zipper Whose Hole Is a Universe · Tropical Petri Nets · The Pflow Square · Structuralism, Not Objects · Earned Compression