Zorn の補題の Agda による証明

なんでそんなものをやるのか

だいたい補題とついてる方が重要

アメリカ人はゾーンと読むだろうけどツォルンな

本当の発音は知りません

役に立つかではなく、単に面白いから

agdaでの集合論の例題として

HOD が Agda での集合

  & : HOD  → Ordinal

  * : Ordinal  → HOD

  *iso   :  {x : HOD }      → * ( & x ) ≡ x

  &iso   :  {x : Ordinal }  → & ( * x ) ≡ x

順序数との対応がある

　　構造体 HOD のアドレスが順序数だと思えばよい

集合論は C と同じ

Agdaと集合論の相性

record Filter { L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where

 field

   filter  : HOD   

   f⊆L     : filter ⊆ L

   filter1 : { p q : HOD } →  L ∋ q → filter ∋ p 

      →  p ⊆ q  → filter ∋ q

   filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  

      → L ∋ (p ∩ q) → filter ∋ (p ∩ q)

教科書の式をほぼ、そのまま書ける ∃とか∀は使わない(だから綺麗)

∃は関数があるってこと。入力変数には∀すべてついている

数学の面倒さの大きな部分が∃と∀と¬ のスコープの問題(かっこ書け

部分と全体

任意の全順序部分集合が上界を持てば極大元がある

    record IsSUP (A B : HOD) (x : Ordinal ) : Set n where

       field

          ax : odef A x

          x≤sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (* y < * x ) 

    record Maximal ( A : HOD )  : Set (Level.suc n) where

       field

          maximal : HOD

          as : A ∋ maximal

          ¬maximal

定義が微妙半順序と全順序上界と極大元

証明が激ムズ載ってない本が多い

(誰も知らない) 応用がすごい

極大部分集合の存在 ⊆は半順序

極大フィルターの存在

コーエンモデル

チコノフの定理 (大抵の初学者はここで落ちる

          自分が落ちたということね

数学はプログラミング

命題の記述は型宣言 (これは容易なことが多い

証明は値、関数の実装

証明の方針は関数の組合せ

Agda は単純な関数型言語 (プログラマならすでに全部知ってる

ほぼ Haskell

字句定義が簡単

   indent base 

   Unicodeで、ほぼ数学書の記述をそのままコードにできる

   ただ、if文に相当するものは複雑 with 文

   単一化/≡は非自明なことが多い 

      これが簡単だったら数学にならない

Agdaの実装自体はかなり複雑

Haskellで書いてある

         ラムダ式の評価

         正規形の一致の判定 単一化

         停止性判定

         単一化の制約 割と謎

         具象化不足の判定

         再帰 record

数学と論理を理解するということは

これを理解するということ

Agdaの証明

証明が終わるとエラー無しで情報があまりない

         inspector が欲しい

         評価はできる

Agda の∧と∨

record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where

   constructor ⟪_,_⟫

   field

      proj1 : A

      proj2 : B

data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where

   case1 : A → A ∨ B

   case2 : B → A ∨ B

Haskell では一つになっている。Curry Howard 対応。

自然演繹に相当する。

Agda の∀と∃

    record SUP ( A B : HOD )  : Set (Level.suc n) where

       field

          sup : HOD

          isSUP : IsSUP A B (& sup)

    s0 : {A B : HOD} → (s : SUP A B) → IsSUP A B ( SUP.sup s )

    s0 {A} {B} s = SUP.isSUP s

入力変数には、∀ と考えてよい

入力変数の record の中に sup : HOD がある。つまり ∃ s : HOD。

一階述語論理は∀と∃が入り混じるから難しい

     infinity : ∃ A ( od∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )

は以下のようになる

     infinite : HOD

     infinity∅ :  od∅ ∈ infinite

     infinity :  ( x : HOD  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite

∃ は関数を作るか、record の field にする。

Agdaでの集合論

自然数の集合

    record NSet : Set (suc zero) where

       field

          def : ℕ → Set 

    eqa1 : NSet

    eqa1 = record { def = λ x →  x * x + 6 ≡ 5 * x   }

2 と 3 が実際に入っている

    _∋_ : NSet → ℕ → Set 

    S ∋ x = def S x

    eq1∋2 : eqa1 ∋ 2

    eq1∋2 = refl

    eq1∋3 : eqa1 ∋ 3

    eq1∋3 = refl

集合の等しさ

    eqa2 : NSet

    eqa2 = record { def = λ x →  (x ≡ 2) ∨ ( x ≡ 3 )   }

    eq2∋3 : eqa2 ∋ 3

    eq2∋3 = case2 refl

    record _==_  ( a b :  NSet  ) : Set  where

      field

         eq→ : ∀ { x : ℕ } → def a x → def b x 

         eq← : ∀ { x : ℕ } → def b x → def a x

自然数の集合の集合

    record NSetSet : Set (suc zero) where

       field

          ndef : NSet → Set

ここまで当たり前過ぎて矛盾が入る余地がない

        本当ですか? だって単なる方程式

        解があるかどうかは知らん 空集合

ここで、ℕ と NSet を同じ物(集合)として扱いたい

実在論的に数学したい

順序数の公理と超限帰納法

順序数の公理

     TransFinite : { ψ : ord  → Set (suc n) }

          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )

          →  ∀ (x : ord)  → ψ x

可算順序数なら単なる数学的帰納法 (induction )

非可算でも成立すると信じる

 < では成立しない (Well-foundedness (最小要素がある)が必要)

 可算順序数は順序数の公理を満たす(モデルがある

集合と順序数とのiso があると仮定する

  & : HOD  → Ordinal

  * : Ordinal  → HOD

  *iso   :  {x : HOD }      → * ( & x ) ≡ x

  &iso   :  {x : Ordinal }  → & ( * x ) ≡ x

ゲーデル数だと思う

あるいは集合の要素の数だと思う

いろいろ怪しい

この仮定が正しいかどうかは決定不能

教科書には載ってる定理。(ZFの公理と、順序数の構成とゲーデル数から出る)

しかし大半は可算順序数

集合は順序数方程式 OD

ではだめ iso と矛盾順序数全体を含むから

         順序数自体は自分自身と対応する集合を持つ

これはℕもそう。デテキント無限。しかし自分自身を含むのはだめ。(ラッセルの逆理)

集合は解に上限がある順序数方程式 HOD

    record OD : Set (suc n ) where

      field

        def : (x : Ordinal  ) → Set n

    record HOD : Set (suc n) where

      field

        od : OD

        odmax : Ordinal

o< は順序数の順序。< とは別。

ODはクラスに相当する。

Agdaでの集合論の公理 ODAxiom

record ODAxiom : Set (suc n) where

 field

  -- HOD is isomorphic to Ordinal (by means of Goedel number)

  & : HOD  → Ordinal

  * : Ordinal  → HOD

  c<→o<  :  {x y : HOD  }   → def (od y) ( & x ) → & x o< & y

  ⊆→o≤   :  {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) 

      → & y o< osuc (& z)

  *iso   :  {x : HOD }      → * ( & x ) ≡ x

  &iso   :  {x : Ordinal }  → & ( * x ) ≡ x

  ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y

Agdaでの集合論の公理 ODAxiom (続き)

下の三つは Zorn の補題では使わない。Aの中で閉じだ議論だから

Uion の存在と無限公理に関係する

  sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) 

     →  Ordinal -- required in Replace

  sup-o≤ :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } 

     → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤  sup-o A ψ

  ho< : {x : HOD} → & x o< next (odmax x)

ODAxiomからのZF公理の導出 (今となっては易しい

すべてを順序数方程式で書けば良い (方針が明確

HODは Set (suc n) 、定義は Set n で書く

record Own (A : HOD) (x : Ordinal) : Set n where

    field

       owner : Ordinal

       ao : odef A owner

       ox : odef (* owner) x

Union : HOD → HOD

Union U = record { od = record { def = λ x → Own U x } ; odmax = osuc (& U) ;

        umax :  {y : Ordinal} → Own U y → y o< osuc (& U)

        umax {y} uy = o<→≤ ( ordtrans (odef< (Own.ox uy)) (subst (λ k → k o< & U) (sym &iso) umax1) ) where

            umax1 : Own.owner uy o< & U

            umax1 = odef< (Own.ao uy)

前のよりも、だいぶ簡単かつ使いやすくなってる

OD.agda

ほとんどすべてのデータ構造を集合に入れられる

直積とか

ZFの公理を使える

HOD使う方が楽 (ただし上限の証明

(やさしいとは言ってない

HOD集合ではなくODな場合がある

    順序数なんか二つとか

    型がないものを入れるな

自然数との対応があれば自動的に入る

          対応があるものの例 List Bool

入らないものは何? (さぁ?

非可算なデータ構造の例 List Bool → Bool

可算順序数と非可算集合注意して扱う必要がある

      順序数は可算だが可算でない

      可算順序数は作れるが集合論のモデルにはならない

           集合は非可算 Power ω を含むから

      集合論は可算モデルを持つが可算ではない

          あらゆる集合には可算順序数と対応する

          要素が入ってる(かもしれん

          レーベルハイムスコーレムの定理

          集合と可算順序数は随伴 (証明してません

          順序数の方程式の解はしょせん可算個

選択公理と排中律は同じもの

   整列定理と選択公理は直観主義論理では分離される

Zorn の補題の証明方針

   極大元があるならよい

   ないなら単調増加関数を選択公理から作れる

   それから無限上昇列を作る

 　全順序部分集合の上昇列(ZChain)をその上界関数から作る

   ZChain の最大性を示す

   最大なら不動点があって、無限上昇列と矛盾する

半順序関係と単調増加関数

    <-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥

    <-irr0 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥

    <-irr0 {a} {b} A∋a A∋b = <-irr

    ≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set n

    ≤-monotonic-f A f = (x : Ordinal ) → odef A x → (  x ≤  (f x) ) ∧  odef A (f x )

    <-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set n

    <-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x < * (f x) ) ∧  odef A (f x )

これと

    fc-stop : ( A : HOD )    ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal }

    → (aa : odef A a ) →(  {y : Ordinal} → FClosure A f a y → (y ≡ b ) ∨ (y << b )) → a ≡ b → f a ≡ a

これが矛盾することになる

FClsoure

fの閉包を証明付きデータ構造で作る

    data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where

       init : {s1 : Ordinal } → odef A s → s ≡ s1  → FClosure A f s s1

       fsuc : (x : Ordinal) ( p :  FClosure A f s x ) → FClosure A f s (f x)

f の可算無限個の繰り返し適用

これは、順序数を飛び回るが、仮定により上界がある

この上界は順序数的にも < 的にも上になるはず

UnionCF A f ay supf x

上の閉包を HOD で集合として定義する

    data UChain  { A : HOD } { f : Ordinal → Ordinal }  {supf : Ordinal → Ordinal} {y : Ordinal } 

       (ay : odef A y )

           (x : Ordinal) : (z : Ordinal) → Set n where

        ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain ay x z

        ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u
          ( fc : FClosure A f (supf u) z ) → UChain ay x z

    UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) 

       ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD

    UnionCF A f ay supf x

       = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ;

           odmax = & A ;

これが、全順序を持つことを調べる

   f-total : IsTotalOrderSet (UnionCF A f ay supf x)

ZChain 鎖

UnionCF A f ay supf x を全順序数に対して超限帰納法で作る

    record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)

            {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where

       field

          supf :  Ordinal → Ordinal

          asupf :  {x : Ordinal } → odef A (supf x)

          is-minsup : {x : Ordinal } → (x≤z : x o≤ z) 

             → IsMinSUP A (UnionCF A f ay supf x) (supf x)

          chain : HOD

          chain = UnionCF A f ay supf z

supf の性質

supf は単調増加

          supf-mono : {a b : Ordinal } → a o≤ b → supf a o≤ supf b

          zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x

supf は前の supf の FClosure の上界

          cfcs  : {a b w : Ordinal } → a o< b → b o≤ z 

             → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w

鎖の最大性

    record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)

            {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where

       supf = ZChain.supf zc

       field

          is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f ay supf z) a ) 

              → b o< z  → (ab : odef A b)

              → HasPrev A (UnionCF A f ay supf z) f b ∨  IsSUP A (UnionCF A f ay supf b) b

              → * a < * b  → odef ((UnionCF A f ay supf z)) b

超限帰納法 (可算順序数の induction で作成する

     SZ : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) 

        → (x : Ordinal) → ZChain A f mf< ay x

     SZ f mf< {y} ay x = TransFinite {λ z → ZChain A f mf< ay z  } (λ x → ind f mf< ay x   ) x

    直後順序数の場合  (直前の UnionCFがある)

    極限順序数の場合 ( x が o∅ の時と、o∅ o< x の時)

          (それ以下の UninCF のUnion )

場合分け

     ind : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) {y : Ordinal} (ay : odef A y) 

         → (x : Ordinal)

         → ((z : Ordinal) → z o< x → ZChain A f mf< ay z) → ZChain A f mf< ay x                             

     ind f mf< {y} ay x prev with Oprev-p x  

     ... | yes op = ?                  

     ... | no lim with trio< x o∅                                                                                                

     ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )

     ... | tri≈ ¬a x=0 ¬c = ?

     ... | tri> ¬a ¬b 0

主な証明

     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) 

         (mf< : <-monotonic-f A f )  (zc : ZChain A f mf< as0 (& A) )

            → (sp1 : MinSUP A (ZChain.chain zc))

            → f (MinSUP.sup sp1)  ≡ MinSUP.sup sp1

     fixpoint = ?

以下は実は不要。fixpoint で既に矛盾を出せる。

     ¬Maximal→¬cf-mono :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-<-monotonic nmx) as0 (& A)) → ⊥

     ¬Maximal→¬cf-mono nmx zc = <-irr0  {* (cf nmx c)} {* c}

           (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.as  msp1 ))))

           (subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )

           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) (cf-is-<-monotonic nmx ) zc msp1  ))) -- x ≡ f x ̄

                (proj1 (cf-is-<-monotonic nmx c (MinSUP.as msp1 ))) where          -- x < f x

          supf = ZChain.supf zc

          msp1 : MinSUP A (ZChain.chain zc)

          msp1 = msp0 (cf nmx) (cf-is-<-monotonic nmx) as0 zc

          c : Ordinal

          c = MinSUP.sup msp1

Maximal のあるなしでの場合分け

     zorn00 : Maximal A

     zorn00 with is-o∅ ( & HasMaximal )

     ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) 

           ; as = zorn01 ; ¬maximal
         -- yes we have the maximal because of the axiom of choice

         zorn03 :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )

         zorn03 =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))   -- Axiom of choice

         zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))

         zorn01  = proj1  zorn03

         zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)

         zorn02 {x} ax m
     ... | yes ¬Maximal = ⊥-elim ( ¬Maximal→¬cf-mono nmx (SZ (cf nmx) (cf-is-<-monotonic nmx) as0 (& A) )) where

         -- if we have no maximal, make ZChain, which contradict SUP condition

         nmx : ¬ Maximal A

         nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where

              zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) 

                 →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y))

              zc5 = ⟪  Maximal.as mx , (λ y ay mx
                 (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx

なぜ、そんなに難しいのか

理由はいろいろある

    一行書くのに三日かかったりする

鎖の定義を工夫する必要がある

       最小上界が必須なのに避けようとしてた

       鎖の最大性自体に無限上昇列が必須

             なのに気が付かなかった

       それ自身が矛盾してるように見える

       数学書の記述は気分だけ、かなりの部分を補う

試行錯誤すると広範な影響

   大きいので遅い

Agdaが遅い問題

  メモリ爆発

   並列処理がない

   Agdaのだめさ

数学はAgdaで記述しろ

集合論は不要

   無意味な複雑さは排中律から来てる

   排中律は命題ごとに個別

   選択公理を明示するなら排中律も明示しろ

Toposで良い

   だが equalizerの扱いが… Agdaの≡に相当

   Topos internal language は表示的意味論そのもの

   お、話が元に戻った

Zorn の補題の Agda による証明なんでそんなものをやるのかだいたい補題とついてる方が重要アメリカ人はゾーンと読むだろうけどツォルンな本当の発音は知りません