Documentation

Formalizations.SetTheory.Ordinal.Gentzen.Acc

Choice-free well-foundedness of ordinal notations below ε₀ #

Mathlib proves that its normal ordinal notations are well founded (NONote.lt_wf), but its order < and normal form ONote.NF on ONote are defined through ONote.repr : ONote → Ordinal, so that proof depends on Classical.choice (through Ordinal.lt_wf).

This file defines a syntactic strict order slt (lexicographic comparison by ONote.cmp) and a syntactic Cantor normal form SNF on Mathlib's ONote, neither of which mentions Ordinal or repr, and proves directly that slt is well founded on syntactic normal forms, by a nested induction (exponent, coefficient, tail) in the style of Gentzen and Schütte. The core results depend only on propext.

A bridge section proves that slt and SNF agree with Mathlib's < and NF; the bridge does use Classical.choice.

Main results #

References #

Syntactic order and normal form (no Ordinal, no repr) #

source
def Gentzen.Acc.slt (a b : ONote) :
Prop

Syntactic strict order on notations: lexicographic comparison by ONote.cmp.

Equations
Instances For
    source
    @[instance_reducible]
    instance Gentzen.Acc.instDecidableSlt (a b : ONote) :
    Decidable (slt a b)
    Equations
    source
    def Gentzen.Acc.topBelow :
    ONote → ONote → Prop

    topBelow a e: the leading exponent of a (if any) is slt-below e.

    Equations
    Instances For
      source
      def Gentzen.Acc.SNF :
      ONote → Prop

      Syntactic Cantor normal form: exponents strictly decreasing (w.r.t. slt), recursively.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance Gentzen.Acc.decTopBelow (a e : ONote) :
        Decidable (topBelow a e)
        Equations
        source
        @[instance_reducible]
        instance Gentzen.Acc.decSNF (a : ONote) :
        Decidable (SNF a)
        Equations

        Constructive facts about Ordering.then and cmp #

        source
        theorem Gentzen.Acc.then_eq_lt {o p : Ordering} (h : o.then p = Ordering.lt) :
        o = Ordering.lt ∨ o = Ordering.eq ∧ p = Ordering.lt
        source
        theorem Gentzen.Acc.then_eq_eq {o p : Ordering} (h : o.then p = Ordering.eq) :
        o = Ordering.eq ∧ p = Ordering.eq
        source
        theorem Gentzen.Acc.natCmp_lt {m n : ℕ} (h : cmp m n = Ordering.lt) :
        m < n
        source
        theorem Gentzen.Acc.natCmp_eq {m n : ℕ} (h : cmp m n = Ordering.eq) :
        m = n
        source
        theorem Gentzen.Acc.eq_of_cmp_eq' {a b : ONote} :
        a.cmp b = Ordering.eq → a = b

        Constructive version of ONote.eq_of_cmp_eq.

        source
        theorem Gentzen.Acc.not_slt_zero (a : ONote) :
        ¬slt a ONote.zero
        source
        theorem Gentzen.Acc.slt_oadd_cases {e : ONote} {n : ℕ+} {a e' : ONote} {n' : ℕ+} {a' : ONote} (h : slt (e'.oadd n' a') (e.oadd n a)) :
        slt e' e ∨ e' = e ∧ ↑n' < ↑n ∨ e' = e ∧ n' = n ∧ slt a' a

        Accessibility #

        source
        def Gentzen.Acc.R (x y : ONote) :
        Prop

        The relation whose accessibility we prove: slt restricted to syntactic normal forms.

        Equations
        Instances For
          source
          theorem Gentzen.Acc.acc_zero :
          Acc R ONote.zero
          source
          def Gentzen.Acc.H (e : ONote) :
          Prop

          H e: every normal notation below ω ^ e is accessible.

          Equations
          Instances For
            source
            theorem Gentzen.Acc.acc_oadd_of_H {e : ONote} (hH : H e) (k : ℕ) (n : ℕ+) :
            ↑n ≤ k → ∀ (a : ONote), Acc R a → SNF (e.oadd n a) → Acc R (e.oadd n a)

            Coefficient/tail step: if everything below ω^e is accessible, so is ω^e·n + a for accessible a (induction on the coefficient bound k, then on Acc a).

            source
            theorem Gentzen.Acc.H_of_acc (e : ONote) :
            Acc R e → H e

            Exponent step (the "accessibility of ω^x" lemma): induction on Acc e.

            source
            theorem Gentzen.Acc.acc_slt (a : ONote) :
            SNF a → Acc (fun (x y : ONote) => SNF x ∧ slt x y) a

            Main theorem: every syntactic normal form is accessible for slt restricted to SNF.

            source
            theorem Gentzen.Acc.wf_slt :
            WellFounded fun (x y : { a : ONote // SNF a }) => slt ↑x ↑y

            Well-foundedness of slt on the subtype of syntactic normal forms.

            source
            theorem Gentzen.Acc.ti_syntactic {P : ONote → Prop} (h : ∀ (a : ONote), SNF a → (∀ (b : ONote), SNF b → slt b a → P b) → P a) (a : ONote) :
            SNF a → P a

            Transfinite induction below ε₀ on syntactic normal forms (choice-free).

            Bridge to Mathlib's < and NF (uses choice) #

            source
            theorem Gentzen.Acc.slt_iff_lt (a b : ONote) [a.NF] [b.NF] :
            slt a b ↔ a < b
            source
            theorem Gentzen.Acc.topBelow_iff (a e : ONote) :
            topBelow a e ↔ e.TopBelow a
            source
            theorem Gentzen.Acc.SNF_iff_NF (a : ONote) :
            SNF a ↔ a.NF

            Checks on samples (by decide) #

            source
            def Gentzen.Acc.samples :
            List ONote

            Samples, in increasing order: 0, 1, 2, ω, ω+1, ω·2, ω^ω.

            Equations
            Instances For