An Order-Theoretic Characterization of Consistent Inductive Inference
Zhou Lu
stat.ML
Sep 23, 2026 · v1
cs.LG
TL;DR
The main order-theoretic characterization of consistent learning and the evidence-stabilization proposition are formalized in Lean 4, with a public repository.
Abstract
When can a learner make only finitely many prediction errors along every infinite sequence labeled by a fixed, unknown hypothesis? We characterize this form of consistency for arbitrary binary hypothesis classes in ZFC, without requiring a uniform mistake bound. The characterization uses a single linear order on finite realizable traces. Each trace selects its least subtrace, and the order must satisfy two conditions: conflicting traces select different subtraces, and the order is well-founded on the traces of each fixed target. These conditions induce a learner whose selected evidence decreases on every mistake. Conversely, a consistent learner yields such an order through canonical mistake transcripts and the Kleene–Brouwer ordering. The result provides a representation of consistent prediction by finite evidence, answering a question of Lu (2024).
Problem
The question is when a learner can make only finitely many prediction errors along every input sequence labeled by a fixed unknown binary hypothesis, without a uniform mistake bound. This answers a question posed by Lu (2024).
Approach
Consistency is characterized in ZFC by a single linear order on finite realizable traces. Each trace selects its least subtrace, conflicting traces must select different subtraces, and the order must be well-founded on each target's traces. The sufficiency direction builds a learner whose selected evidence strictly decreases on every mistake. The necessity direction uses canonical mistake transcripts and the Kleene–Brouwer ordering. The main theorem and the stabilization proposition are formalized in Lean 4.
Results
A hypothesis class is consistent if and only if such an order exists. Selected evidence eventually stabilizes along each target. On countable domains, a class is consistent if and only if it is countable. Choice is shown to be necessary for the converse over arbitrary domains.
