Documentation

InfinitaryLogic.Descriptive.TreeCodes

Tree codes, the continuous Kleene–Brouwer code, and analytic boundedness for well-founded trees #

Classical background: Gao, Invariant Descriptive Set Theory (CRC Press, 2009), Theorem 1.6.11 (boundedness for well-founded trees) and Exercise 1.5.7 (the Kleene–Brouwer equivalence).

The code-level form of the Kleene–Brouwer material (issue #73), on top of the raw combinatorics in Descriptive/KleeneBrouwer.lean and the analytic boundedness for coded well-orders (#64).

Codes #

A code c : StructureSpace L with a distinguished unary mem : L.Relations 1 names the set of finite sequences x whose node code Equiv.listNatEquivNat x satisfies mem (nodeSet). treeClass mem is the set of codes naming a prefix-closed set; it is closed (isClosed_treeClass, a countable intersection of clopen coordinate conditions) hence Borel. wellFoundedTreeClass mem adds "no infinite branch", as a descending chain in strict extension; no analyticity is claimed for it.

The Kleene–Brouwer code #

kbCode mem c is a code in the dedicated one-binary-relation language kbLanguage, whose symbol kbRelSym.lt is a strict order: the nodes of the named set come first, in Kleene–Brouwer order, and every other natural afterwards, in the usual order (kbRel). A dedicated language, rather than Mathlib's Language.order, so that no ≤-named symbol is published with strict semantics. Each coordinate of kbCode mem c is a function of two membership bits of c and the two naturals, so kbCode is continuous (continuous_kbCode), not merely Borel.

For a well-founded tree code kbRel is the lexicographic sum of KB on the nodes and < on the rest (kbSumEmbedding), hence a well-order: kbCode_mem_wellOrderClass. The tree's rank, treeRank mem hwf, is the height of strict extension on its tree and takes the well-foundedness proof rather than defaulting on ill-founded codes; treeRank_le_type_kbCode bounds it by the order type of the KB code, for any well-ordering proof, through the embedding of the nodes.

Boundedness #

analytic_wellFoundedTree_rank_boundedness: an analytic family of well-founded tree codes has ranks bounded by one ordinal below ω₁. The image under the continuous kbCode is an analytic family of well-orders, so #64's analytic_wellOrder_type_boundedness bounds the KB order types, hence the ranks. exists_rank_bound_of_dominated is the domination adapter: parameters each dominated by some tree of such a family have uniformly bounded assigned ranks, with no topology on the parameter space.

The Kleene–Brouwer target language #

source
inductive FirstOrder.Language.kbRelSym :
ℕ → Type

The single relation symbol of the KB language: a strict order.

Instances For
    source
    def FirstOrder.Language.kbLanguage :
    Language

    The dedicated one-binary-relation language the Kleene–Brouwer code lands in. Its only symbol is the strict order kbRelSym.lt.

    Equations
    Instances For
      source
      instance FirstOrder.Language.kbLanguage.instIsRelational :
      kbLanguage.IsRelational
      source
      instance FirstOrder.Language.kbLanguage.instSubsingletonRelations (n : ℕ) :
      Subsingleton (kbLanguage.Relations n)
      source
      @[instance_reducible]
      instance FirstOrder.Language.kbLanguage.instUniqueSigmaNatRelations :
      Unique ((n : ℕ) × kbLanguage.Relations n)
      Equations
      source
      instance FirstOrder.Language.kbLanguage.instCountableSigmaNatRelations :
      Countable ((n : ℕ) × kbLanguage.Relations n)

      Trees named by codes #

      source
      @[reducible, inline]
      abbrev FirstOrder.Language.nodeCode (x : List ℕ) :
      ℕ

      The node code of a finite sequence.

      Equations
      Instances For
        source
        def FirstOrder.Language.nodeSet {L : Language} (mem : L.Relations 1) (c : L.StructureSpace) :
        Set (List ℕ)

        The set of sequences a code names through mem.

        Equations
        Instances For
          source
          def FirstOrder.Language.treeClass {L : Language} (mem : L.Relations 1) :
          Set L.StructureSpace

          The tree class: codes whose named set is prefix-closed.

          Equations
          Instances For
            source
            def FirstOrder.Language.treeOf {L : Language} (mem : L.Relations 1) (c : L.StructureSpace) (hc : c ∈ treeClass mem) :
            ↥(Descriptive.tree ℕ)

            The tree a code in the tree class names.

            Equations
            Instances For
              source
              @[simp]
              theorem FirstOrder.Language.mem_treeOf {L : Language} {mem : L.Relations 1} {c : L.StructureSpace} (hc : c ∈ treeClass mem) {x : List ℕ} :
              x ∈ treeOf mem c hc ↔ x ∈ nodeSet mem c
              source
              def FirstOrder.Language.wellFoundedTreeClass {L : Language} (mem : L.Relations 1) :
              Set L.StructureSpace

              The well-founded tree class: tree codes with no infinite branch.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem FirstOrder.Language.treeClass_subset {L : Language} (mem : L.Relations 1) :
                wellFoundedTreeClass mem ⊆ treeClass mem

                The Kleene–Brouwer relation on ℕ induced by a code #

                source
                def FirstOrder.Language.kbRel {L : Language} (mem : L.Relations 1) (c : L.StructureSpace) (x y : ℕ) :
                Prop

                The KB relation on node codes: nodes of the named set first, in KB order; the remaining naturals afterwards, in their own order. Depends only on the two membership bits and the two naturals.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[instance_reducible]
                  instance FirstOrder.Language.instDecidableRelNatKbRel {L : Language} (mem : L.Relations 1) (c : L.StructureSpace) :
                  DecidableRel (kbRel mem c)
                  Equations
                  source
                  def FirstOrder.Language.kbCode {L : Language} (mem : L.Relations 1) (c : L.StructureSpace) :
                  kbLanguage.StructureSpace

                  The Kleene–Brouwer code: the kbLanguage-code of kbRel.

                  Equations
                  Instances For
                    source
                    theorem FirstOrder.Language.kbCode_le {L : Language} (mem : L.Relations 1) (c : L.StructureSpace) (v : Fin 2 → ℕ) :
                    kbCode mem c ⟨⟨2, kbRelSym.lt⟩, v⟩ = decide (kbRel mem c (v 0) (v 1))

                    Continuity: each coordinate depends on two bits #

                    source
                    theorem FirstOrder.Language.continuous_kbCode {L : Language} (mem : L.Relations 1) :
                    Continuous (kbCode mem)

                    kbRel is a well-order on a well-founded tree code #

                    source
                    @[instance_reducible]
                    instance FirstOrder.Language.instDecidablePredNatIsNode {L : Language} (mem : L.Relations 1) (c : L.StructureSpace) :
                    DecidablePred (FirstOrder.Language.IsNode✝ mem c)
                    Equations
                    source
                    theorem FirstOrder.Language.isWellOrder_kbRel {L : Language} (mem : L.Relations 1) {c : L.StructureSpace} (hwf : c ∈ wellFoundedTreeClass mem) :
                    IsWellOrder ℕ (kbRel mem c)
                    source
                    theorem FirstOrder.Language.relMap_kbCode {L : Language} (mem : L.Relations 1) (c : L.StructureSpace) (x y : ℕ) :
                    Structure.RelMap kbRelSym.lt ![x, y] ↔ kbRel mem c x y

                    The decoded relation of the KB code is kbRel.

                    source
                    theorem FirstOrder.Language.kbCode_mem_wellOrderClass {L : Language} (mem : L.Relations 1) {c : L.StructureSpace} (hwf : c ∈ wellFoundedTreeClass mem) :
                    kbCode mem c ∈ wellOrderClass kbRelSym.lt

                    A well-founded tree code has a well-ordered KB code.

                    The rank of a well-founded tree code #

                    source
                    noncomputable def FirstOrder.Language.treeRank {L : Language} (mem : L.Relations 1) {c : L.StructureSpace} (hwf : c ∈ wellFoundedTreeClass mem) :
                    Ordinal.{0}

                    The rank of a well-founded tree code: the height of strict extension on its tree. Takes the well-foundedness proof; no default value on ill-founded codes.

                    Equations
                    Instances For

                      The tree class is closed (hence Borel) #

                      source
                      theorem FirstOrder.Language.isClosed_treeClass {L : Language} (mem : L.Relations 1) :
                      IsClosed (treeClass mem)

                      The tree class is a countable intersection of clopen coordinate conditions: for each x and a, "x ++ [a] named implies x named".

                      source
                      theorem FirstOrder.Language.measurableSet_treeClass {L : Language} (mem : L.Relations 1) [Countable ((l : ℕ) × L.Relations l)] :
                      MeasurableSet (treeClass mem)

                      Boundedness #

                      source
                      @[reducible, inline]
                      abbrev FirstOrder.Language.kbCodeRel {L : Language} (mem : L.Relations 1) (c : L.StructureSpace) (x y : ℕ) :
                      Prop

                      The decoded relation of the KB code, as a relation on ℕ.

                      Equations
                      Instances For
                        source
                        theorem FirstOrder.Language.treeRank_le_type_kbCode {L : Language} (mem : L.Relations 1) {c : L.StructureSpace} (hwf : c ∈ wellFoundedTreeClass mem) (h : IsWellOrder ℕ (kbCodeRel mem c)) :
                        treeRank mem hwf ≤ Ordinal.type (kbCodeRel mem c)

                        The rank is at most the order type of the KB code, for any well-ordering proof.

                        source
                        theorem FirstOrder.Language.analytic_wellFoundedTree_rank_boundedness {L : Language} [Countable ((l : ℕ) × L.Relations l)] (mem : L.Relations 1) {A : Set L.StructureSpace} (hA : MeasureTheory.AnalyticSet A) (hWF : A ⊆ wellFoundedTreeClass mem) :
                        ∃ β < (Cardinal.aleph 1).ord, ∀ (c : L.StructureSpace) (hc : c ∈ A), treeRank mem ⋯ < β

                        Analytic boundedness for well-founded trees on a countable alphabet. An analytic family of well-founded tree codes has ranks bounded below ω₁.

                        source
                        theorem FirstOrder.Language.exists_rank_bound_of_dominated {L : Language} [Countable ((l : ℕ) × L.Relations l)] (mem : L.Relations 1) {A : Set L.StructureSpace} (hA : MeasureTheory.AnalyticSet A) (hWF : A ⊆ wellFoundedTreeClass mem) {X : Type u_1} {B : Set X} (rank : X → Ordinal.{0}) (hdom : ∀ x ∈ B, ∃ (c : L.StructureSpace) (hc : c ∈ A), rank x ≤ treeRank mem ⋯) :
                        ∃ β < (Cardinal.aleph 1).ord, ∀ x ∈ B, rank x < β

                        The domination adapter: parameters each dominated by some tree of an analytic family of well-founded trees have uniformly bounded ranks. No topology on the parameter space.