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.
That axis is past-tense. The paper doesn't frame it that way, but every construction in it reads as a monotone accumulator over completed observations. The tropical core has been drawing the same axis coordinate by coordinate in every post. Their Theorem 8.4 — that the ω² layer cannot be collapsed without classical logic — is the independent result we needed for the claim that the past/future boundary is structural.
Paper: arXiv:2602.10844 — Generalized Decidability via Brouwer Trees, with a Cubical Agda formalization.
α-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 finite-k classes (ω·k) collapse together — semidecidability absorbs them. The ω² and higher layers do not collapse.
Brw is a quotient inductive-inductive type with three constructors: zero, succ, and limit (f : ℕ → Brw) where limit accepts only strictly increasing sequences.
The strict-increase constraint is load-bearing. Ordinary ordinals accept any sequence under sup, which is why they can be classically well-ordered. Brouwer ordinals only take a limit when strict progress has been witnessed — so limit f carries not just the function but evidence that each step advanced. 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. The ordinal witness totally orders a given history; it does not totally order independent histories.
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. It never retracts. It ends in a limit of strict progress. An ordinal that grows with observation is a past-tense object — the history compressed to its order type.
Theorem 8.4 is the structural payoff. Under countable choice, every finite-k α-decidable proposition (α = ω·k) is semidecidable. The obvious hope — that with enough choice you can flatten the quantifier-alternation layer at ω² — is false.
Collapsing ω²-decidable to semidecidable would prove MP ⇒ LPO. Markov's Principle does not imply the Limited Principle of Omniscience constructively. So the collapse is impossible even with countable choice.
The ∀n. semidec(n) step — the jump from ω·2 to ω² — is not a convenience of presentation. It is a constitutive layer. Quantifier alternation cannot be absorbed into a single-pass observation process, even with choice.
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.
This is Bove–Capretta (Modelling general recursion in type theory) adapted from partial functions to higher inductive types. It applies to any function out of a QIIT carrier — marking quotients, Chu-space equalities, forgetful functors between net categories.
P ↔ α ≤ y reads as: P holds exactly when the accumulator has crossed the threshold. The accumulator grows under observation. The threshold is fixed. The future-tense claim — P will hold — is equivalent to a past-tense fact: y has grown past α.
This is the adjunction hinge the tense type theory post drew around execution state. The present is where the past (accumulator) meets the future (predicate). The paper draws exactly this picture, without calling it tense.
The ordinal tells you 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 is not about how long the proof is. It is about how much history the witness has to compress.
The tropical core carries a marking T : Place → ℝ ∪ {∞} — a vector past, one coordinate per place. Their framework carries y : Brw — a scalar past, one ordinal total.
Specialize to a one-place linear net. Tropical composition reduces to min-plus on a single coordinate, which is order-isomorphic to Brouwer ordinal accumulation. Ψₙ of a proposition should match the tropical marking at step n of the corresponding single-place net. Their framework is the scalar case; the tropical framework is the vector extension.
The extension is not free. Vector past has one accumulator per place; independent places accumulate independently, and the past state factorizes along the place-set. Pointwise order on Place → ℝ ∪ {∞} is partial — two markings can be incomparable. Brouwer ordinals are prelinear; markings are genuinely partial.
Two independent firings in a Petri net can happen in either order without changing the final marking. An ordinal witness distinguishes them. Picking an ordinal-valued accumulator implicitly picks a schedule.
A concurrent past needs an accumulator invariant under Mazurkiewicz equivalence of firing sequences. Brouwer ordinals are the wrong carrier for that — not because the authors missed something but because the structure is total enough that it cannot represent independence. The analogue that works is a Brouwer-indexed diagram over a partial order: event structures, pomset-indexed limits, or a Brouwer poset.
The paper does not construct one. That is where the scalar framework stops and the vector tropical framework has to begin.
The past is an ordinal when it's scalar. The past is a tropical marking when it's vector. The ω² obstruction says the boundary between past and future is not a convention — it is a structural layer that classical logic is required to collapse.
Related: Tense Type Theory · Tropical Petri Nets · Earned Compression