Gold's Theorem and Mind Change Characterization

The foundational results of inductive inference theory.

theorem gold_theorem (X : Type u) [Countable X] [DecidableEq X] (C : ConceptClass X Bool) (h_finite : ∀ (S : Finset X), (fun (x : X) => decide (x ∈ S)) ∈ C) (h_infinite : ∃ c ∈ C, {x : X | c x = true}.Infinite) : ¬EXLearnable X C

Gold's theorem (1967): No learner can EX-identify any concept class containing all finite subsets plus some infinite set, from text.

theorem mind_change_characterization (X : Type u) (C : ConceptClass X Bool) : EXLearnable X C ↔ ∃ (L : GoldLearner X Bool), ∀ c ∈ C, ∀ (T : TextPresentation X c), MindChangeOrdinal X L c T.toDataStream < Ordinal.omega0

Mind change characterization: EX-learnable iff every text presentation has finite mind change ordinal. With correctness encoded in MindChangeOrdinal, < omega0 captures both correct convergence and finite mind changes.