Agda 上でのZF集合論の構成
Menu Menu
数学をプログラミングする
プログラミングとはデータ構造をλ項で処理すること数学を直観主義論理を使ってλ項で取り扱える
証明を値として関数型プログラミングするだけで数学になる
ZF集合論を Agda を使ってプログラムしてみる
目標は
ZF集合論のモデルをAgda上に作る
モデルに必要な仮定を明らかにする
公理をAgdaで記述し、モデルがそれを満たすことを示す
これにより集合論の(いくつかの仮定を含む)整合性が示せる
ZF in Agda https://github.com/shinji-kono/zf-in-agda
なんで集合論か
集合論ができればなんでもできそう初学者がつまづく部分(特に選択公理)
結構量が多く、自己参照的な理論がわかりにくい
老後に取っておこうと思ったが、既に老後だからやるべき
5月から9月くらいでモデルの構築までできた
Agda と直観主義論理
カーリーハワード対応とは、命題と証明の関係が、項の型とλ項の関係に対応すること対応するような論理と型つきλ計算を作る
複雑な型も変数の値になれる型つきλ計算(System FC)を使う
First class Type / Dependent Type
ここでは Haskell に近い構文を持つ Agda を使う
(Coq の方が証明に特化しているので広く使われているかも)
Agda 入門
length : {A : Set } → List A → Nat
length [] = zero
length (_ ∷ t) = suc ( length t )
超普通な関数型言語。基本型はSetしかない。型宣言は必須
{} で宣言された入力は推論可能であれば省略できる
data ( Sum type )
複数の constructor を持つデータ型。C の Union、Scalaの Case Class に相当するHaskell の data と共通の構文だが若干の差がある
data List (A : Set ) : Set where
[] : List A
_∷_ : A → List A → List A
_は中置/前置/後置演算子を表す。_を明示すれば普通の関数として使える
data Nat : Set where
zero : Nat
suc : Nat → Nat
A → B は 「A ならば B」
Agdaは型を値として扱える。Dependent tyoe と呼ばれる。型は Set という名前になっている。
ex3 : {A B : Set} → Set
ex3 {A}{B} = A → B
A → B は型Aから型Bを返す関数の型(Set)を表す。これが「A ならば B」という論理式に対応する
型が論理式、その値が証明
A → B は論理式Aから論理式Bへの推論とも言えるし、Aの証明からBの証明を返す関数だとも言える
introduction と elimination
論理式の構文に対しては introduction と elimination がある。
intro 記号を作る / constructor / 導入 elim 記号を使う / accessor / 除去自然演繹(Natural deduction)では
A
:
B A A → B
------------- →intro ------------------ →elim
A → B B
Agda では以下のようになる。→の導入の証明にはλを使う。
→intro : {A B : Set } → A → B → ( A → B )
→intro _ b = λ x → b
→elim : {A B : Set } → A → ( A → B ) → B
→elim a f = f a
重要
{A B : Set } → A → B → ( A → B )
は
{A B : Set } → ( A → ( B → ( A → B ) ))
A → B の証明には
→の左を引数と見て用意してやればよい。(Coq の intros)
ex5 : {A B C : Set } → A → B → C → ?
ex5 a b c = ?
? は hole と呼ばれ、まだ決めてないところ。そこにどんな型が入るべきかは Agda が教えてくれる。
? を全部埋めて、赤(型の不整合)、黄(証明不足、値が不定)、停止性の警告などが出てこなければ証明終了。
A ∧ B
良く知られた conjunctionの 導入 除去は自然演繹では以下のようになる
A B A ∧ B A ∧ B
------------- ----------- proj1 ---------- proj2
A ∧ B A B
これを実現する構造を関数型言語に入れれば良い。
record
record _∧_ A B : Set
field
proj1 : A
proj2 : B
_∧_ は中置演算子を表す。 _∧_ A B は A ∧ B とかける。(Haskell では (∧) を使う)
型Aと型Bから作るデータ構造である。オブジェクトあるいは構造体だと思って良い。
record { proj1 = x ; proj2 = y }
が constructor であり導入になる。
ex3 : {A B : Set} → A → B → ( A ∧ B )
ex3 a b = record { proj1 = a ; proj2 = b }
ex1 : {A B : Set} → ( A ∧ B ) → A
ex1 a∧b = proj1 a∧b
a∧b は変数。空白がないと一続きのシンボルだと思われる。: の前後にも空白が必要。
record は再帰定義も可能だがめんどくさい。
数学的構造
関連する要素の型とその間の関係(公理)が数学的構造を構成する論理関係には順序がない 関数の引数と戻り値には順序がある
なので以下のように書くと良い
record IsOrdinals {n : Level} (ord : Set n)
(_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
field
Otrans : {x y z : ord } → x o< y → y o< z → x o< z
record Ordinals {n : Level} : Set (suc (suc n)) where
field
ord : Set n
_o<_ : ord → ord → Set n
isOrdinal : IsOrdinals ord _o<_
IsOrdinals には順序に関係しない公理を書く。Ordinals の引数には入力を書く。Ordinals の field には Ordinals が提供する存在物を書く。
モデルと理論
record は型なので入力にはいつでも書ける。しかし、それは実在するのか?実際に値を構成してやれば実在することがわかる。つまり、IsOrdinals のfiled = 公理をすべて恒真にする Ordinals の存在物を作ってやればよい
recordの型 = 理論 recordの値 = モデルこれはモデルと呼ばれる。数学的構造(=理論)はモデルが存在すれば無矛盾である(当たり前)
postulate と module
module はAgdaの証明を分割する。 巨大な record に相当するpostulate は仮定。Agda で証明できないもの(たくさんある)を証明抜きつまり型だけで宣言する
postulate
sup-o : ( Ordinal → Ordinal ) → Ordinal
sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ
これは上界の存在を仮定している
postulate と module の入力に書くのとは同等だが、postulateは証明の途中に書けるで途中で定義したものを使える
postulate が構成可能でない場合もある
postulate が矛盾している可能性もある
A ∨ B
data _∨_ (A B : Set) : Set where
case1 : A → A ∨ B
case2 : B → A ∨ B
Haskellと同様にcase1/case2はパターンマッチで場合分けする。
ex3 : {A B : Set} → ( A ∨ A ) → A
ex3 = ?
場合分けには、? の部分にcursolを合わせて C-C C-C すると場合分けを生成してくれる。
ex3 : {A B : Set} → ( A ∨ A ) → A
ex3 (case1 x) = ?
ex3 (case2 x) = ?
∨ の証明図はめんどうなので省略。
Negation
⊥
------------- ⊥-elim
A
矛盾からは何でも導くことができる。この場合、A はSetである。⊥ を導入する推論規則はない。これは、contructor のない data で表すことができる。
data ⊥ : Set where
⊥-elim は以下のように証明できる。
⊥-elim : {A : Set } -> ⊥ -> A
⊥-elim ()
⊥ を使って否定は以下のように定義される。
¬_ : Set → Set
¬ A = A → ⊥
Eqaulity
Agdaの値はすべて項であり、λ式としての正規形が等しいならば同じ。変数が含まれている場合は単一化が可能ならば等しいことになる。
{ x : A } x ≡ y f x y
--------------- ≡-intro --------------------- ≡-elim
x ≡ x f x x
これを data を使った以下のように表す。
data _≡_ {A : Set } : A → A → Set where
refl : {x : A} → x ≡ x
同値関係
refl' : {A : Set} {x : A } → x ≡ x
refl' = ?
sym : {A : Set} {x y : A } → x ≡ y → y ≡ x
sym = ?
trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
trans = ?
cong : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y
cong = ?
順序
一般的に関係は
A → A → Setという形で表される。順序などは、これを data なり述語なりで定義することにより得られる。
data _≤_ : Rel ℕ 0ℓ where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
Qunatifier
入力に条件は付けられないので∀が付いているのと同じ (∀を明示すると型推論してくれる)
∃は Agda にはない。なので、
∃ (x : A ) → p x = ¬ ( ( x : A ) → ¬ ( p x ) )
を使うか、f : A を使って
p fとする。関数を使うと大域的に定義されてしまうので、式の内部での∃ xよりも強い意味になる
こんなんで数学できるのか?
全部できる。実際に、Pricipia Mathematica という Russel Whitehead の巨大な著作がある(が Computer supported でない)この話は基本的にはそれの焼き直し (でもPricipia Mathematicaは ZF集合論とは違う方法を使っている)
record で数学的構造を定義する
変数に証明が入っていると思って、推論をプログラムするという感じ
Agda で証明できない部分
Internal parametricity というのがダメらしい。Free therom が証明できないので圏論のFunctorのuniqunessが示せないFunctional extenstionality が示せない
(∀ x → f x ≡ g x) → f ≡ g排中律が示せない
a ∨ ( ¬ a )なので、(A → B) → ¬ B → ¬ A は証明できるが、 ( ¬ B → ¬ A ) → A → B はだめ
停止性や型推論能力で正しくても証明できないことがある(努力と工夫でなんとかなることも
これらを仮定することは問題ない
ZF集合論の流れ
通常はZFを仮定してZFのモデルを構築して集合論の無矛盾性を証明すると言う流れ
その途中で順序数を使う
Agda では順序数を作ってから順序数定義可能集合(Ordinal Definable Set/ OD)を使う
その時に非構成的な仮定がいくつか必要となる
その仮定を信じるとAgda上で集合論のモデルが構築できると言う流れ
まず順序数を定義する
record Ordinals {n : Level} : Set (suc (suc n)) where
field
ord : Set n
o∅ : ord
osuc : ord → ord
_o<_ : ord → ord → Set n
isOrdinal : IsOrdinals ord o∅ osuc _o<_
まだモデルは構築してないが、単に∅と順序を持つというだけ。osuc は「一つ大きい順序数」
Nat と異なり具体的な構造物になってない。高階の無限を含むと期待される。
順序数の公理
無限に成り立つと期待される性質。超限帰納法も要求する。割り込まれない直後順序数osucが存在する。
直前の順序数が存在しない場合は極限順序数という(そういうものが無限)
大きさは必ず比較できる(全順序)
record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord )
(osuc : ord → ord )
(_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
field
Otrans : {x y z : ord } → x o< y → y o< z → x o< z
OTri : Trichotomous {n} _≡_ _o<_
¬x<0 : { x : ord } → ¬ ( x o< o∅ )
<-osuc : { x : ord } → x o< osuc x
osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
TransFinite : { ψ : ord → Set (suc n) }
→ ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
→ ∀ (x : ord) → ψ x
具体的な順序数を作る
レベルが入っているリストのような構造を作る。これは単なる二次元配列と見なせる
data OrdinalD {n : Level} : (lv : Nat) → Set n where
Φ : (lv : Nat) → OrdinalD lv
OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
これに順序を入れる
data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where
Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x
s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y
これは単なるデータ構造であり、抽象的な仮定を含んでない可算データ構造になっている。
Φ 0 OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2))) Osuc 0 (Φ 0) d< Φ 1
順序数のモデル
これが順序数の公理を満たすことは容易に示せる。(可算順序数の一種)
公理を満たす具体的な構造をモデルという
公理が恒真になるモデルなら、モデルで考えたことは、公理を満たす任意の理論で正しい
モデルがあるなら理論は無矛盾例えば非ユークリッド幾何のモデルをユークリッド空間に埋め込まれた局面上に構築するとか
モデルを使って公理をデバッグする
公理が正しく書かれているかはモデルに対して恒真かどうかでわかるモデルを修正する場合もある。順序の定義とか
入力は仮定だが、その入力は実在するのか?
可算順序数って実数を含んでるの?
順序数は公理的には任意のレベルの無限集合を含んでいるので、その通りモデル化されてた実数を論理的に取り扱う時に、使う実数は可算個しか出てこない
外から見た時には可算
中から見た時には非可算
可算非可算の定義は同じだが対象が異なる
今回はこの定義はしてない
集合の濃度の定義が必要
集合って何?
AgdaのSetは集合ではなくて型 (だったら、なんで Set なんていう名前にしたの?)素朴実在論的には有限個の集まり = リスト
しかし、入っている型はばらばらなので、常に同じ型が入っている Agda のリストとは違う
Set ならばなんでも入るはずだが、今度は Nat の値などが入らない
有限個なら有限個の∨で書けるが...
いや、入っているものは別になんでもいいんじゃない?
φ {φ} {φ,{φ}}, {φ,{φ},...}
これを可算無限繰り返して全部まとめたものを考えて、さらにそれを繰り返す。これ全部をVとする。
この操作はZF集合論でできる。従来の集合論はZFを仮定するのでそれで良い。
しかし、ここでは仮定してない。なのでできない。Vの代わりに順序数を使う。
順序数定義可能集合 (Ordinal Definable Set)
順序数の部分集合を述語で定義する。部分集合っ何?
順序数一つを入力する述語を順序数定義可能集合 (Ordinal Definable Set) OD とする
record OD : Set (suc n ) where
field
def : (x : Ordinal ) → Set n
順序数全体は集合論の意味での集合ではない。順序数全体は
record { def = λ x → true }
で表すことができるので、ODは集合論の意味での集合よりも広い。(が気にしない)
OD での ∋
ODは順序数で判定していて、ODがODの要素となるようになってない。そこで、
od→ord : OD → Ordinal
というODから順序数への対応があると仮定する。すると、あるODがODの要素になるかどうかをdef を使って判定できる。つまり、
A ∋ x を
_∋_ : ( A x : OD ) → Set n
_∋_ A x = def A ( od→ord x )
と定義する。 ψ : Ordinal → Set に対して、A が record { def = λ x → ψ x } とすると、
a x = def A ( od→ord x ) = ψ (od→ord x)
となる。
ODとOrdinalの一対一対応
さらに一対一対応を要求する。
od→ord : OD → Ordinal
ord→od : Ordinal → OD
oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
これは集合論で証明できるらしい。ここでは非構成的な仮定とする。
postulate なので対応は全域ではないらしい。(ちょっと怪しい部分)
最大の順序数がある、つまり、Ordinal の部分集合に対応すると明示する方が良いが、うまくできてない。
ODとOrdinalの順序の保存
Ordinal には順序があるが、ODには包含関係の順序(def)がある。
def y ( od→ord x )
この順序がある場合は、要素が先に定義されている必要がある。つまり、含まれている要素は集合よりも小さい順序数を持つと考えられる。
c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
この順序の対応も集合論では証明できる。ここでは仮定する。
ODは対応する順序数による順序があるが、それに対応するdefがあるわけではない。つまり、これの逆、
o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x
を仮定することはできない。仮定するとと、∀ x ∋ ∅ が証明されてしまい、ODは順序数だけになってしまう。
ISO
順序数とODは 1対1対応なので
oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
を仮定する。
さまざまな集合
述語で定義できる集合の階層はLと呼ばれるまとめると
ZFの公理を直観主義論理に合わせる
ODをZFの集合としてZFの集合論に対応する record を定義するつまり公理をAgdaで記述する
しかし、それがそのままValidになるとは限らない → デバッグする
公理によって扱いが異なる
純論理的な公理
空集合、対、分出、ε-induction、infinityこれらはODの論理的な関係に帰着される
empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
infinity∅ : ∅ ∈ infinite
infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ( x , x ) ) ∈ infinite
ε-induction : { ψ : OD → Set (suc n)}
→ ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
→ (x : OD ) → ψ x
fininity はAgdaのdataとして構築する
data infinite-d : ( x : Ordinal ) → Set n where
iφ : infinite-d o∅
isuc : {x : Ordinal } → infinite-d x →
infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
Union (x , ( x , x )) はxの直後順序数に対応するODなはずだが、それは証明できない
対の公理
対の公理は田中先生の本では
∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y)
となっている。この場合の問題は ∃ z である。これを (x , y) とする。これは _,_ という関数である。
(_,_ : ( A B : ZFSet ) → ZFSet)
これを使うと双方向の矢印を分解して
pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
となる。これは、既に Agda の構文であり、これが公理となる。入力には ∀ がついていると考えて良い。
ODでの pair
OD は順序数の方程式なので、pairの公理に論理式をそのまま書けばよい。
_,_ : OD → OD → OD
x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) }
≡ は項のequality だが、ここで比較しているのは順序数であることを覚えておく。
対の公理の恒真性
ZFSet がODであると仮定して実際に pair→ を証明に行く。
pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y )
pair→ x y t p = ?
ここで p は ( x , y ) ∋ t のこと、つまり、 def ( x , y ) つまり、(t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) である。
_∨_ は data なので(C-c C-c : agda2-make-case )で展開できる。
pair→ x y t (case1 t≡x ) = ?
pair→ x y t (case2 t≡y ) = ?
この?は、( t == x ) ∨ ( t == y ) なので、やはり data _∨_ である。つまり、
pair→ x y t (case1 t≡x ) = case1 ?
pair→ x y t (case2 t≡y ) = case2 ?
となる。? の片方は t == x で、t≡x からこれを作ってやれば良い。t≡x は変数名だが型は
t≡x : od→ord t ≡ od→ord x
というものだと Agda が (C-C C-E : agda2-show-context )で教えてくれる。
しかし、== が何かをまだ定義してなかった。
ODの等号と外延性の公理
ODは述語で定義されているので、その等号を述語のλ項の正規形の等しさで調べると要素が等しいなら集合として等しいという考えよりも狭くなってしまう。外延性の公理は要素が等しい集合は、他の集合から含まれる場合には、同じ扱いになることを要求する。
∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
これはそのまま Agda で書くことができて
extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w )
となる。( A ∋ z ) ⇔ (B ∋ z) をそのまま等号の定義して採用して、 A ∈ w ⇔ B ∈ w を示せると良い。
それには x == y を以下のように定義する。
record _==_ ( a b : OD ) : Set n where
field
eq→ : ∀ { x : Ordinal } → def a x → def b x
eq← : ∀ { x : Ordinal } → def b x → def a x
実際、(z : OD) → (A ∋ z) ⇔ (B ∋ z) ならば A == B であることを示せる。
extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
eq→ (extensionality0 {A} {B} eq ) {x} d = ?
eq← (extensionality0 {A} {B} eq ) {x} d = ?
? は def B x と def A x だが、eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) から生成できる。
実際には diso と置換を含む少し複雑な式になる。
eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
外延性の公理の恒真性
A == B から (w ∋ A) ⇔ (w ∋ B) を導ければ外延性の公理の恒真性を示せるが、それはできそうにない。そこで、
==→o≡ : { x y : OD } → (x == y) → x ≡ y
を仮定する。
extensionality : {A B w : OD } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
この仮定は同じ動作をする述語の同値類を得られるというような仮定になっている。
ここまでの非構成的な仮定のまとめ
ODと順序数の対応(実際には順序数の部分への対応でるあるべき)と、順序の片方向の保存さらに == からODの項としての同一性を導く仮定を使用する。
od→ord : OD → Ordinal
ord→od : Ordinal → OD
oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
==→o≡ : { x y : OD } → (x == y) → x ≡ y
否定形を持つ公理
Union、置換公理これらは論理的な関係としての∃を含んでいるので否定を含む形しか証明できない
置換公理は仮定した上界を使うので非構成的な公理になる
置換公理は任意の順序数上の関数の上界の存在を仮定している。これは非構成的な仮定である
冪集合の公理は
power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x )
power← : ∀( A t : ZFSet ) → t ⊆_ A → Power A ∋ t
のように二重否定を使う必要がある。(恒真性の証明の都合) 排中律を仮定すれば A ∋ x となる。
Union
もとの形は
∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
となっている。 Union では a ⊇ ∃ b ∋ x のような中間的な集合の存在が要求される。これには否定形の∃を使う
union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
OD での Union の定義は以下のようにする。
Union : OD → OD
Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
恒真性の証明は
union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
union← X z UX∋z = FExists _ lemma UX∋z where
lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
と比較的短い。FExists は
FExists : {m l : Level} → ( ψ : Ordinal → Set m )
→ {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
→ (exists : ¬ (∀ y → ¬ ( ψ y ) ))
→ ¬ p
FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
つまり、否定で定義された存在記号を対偶で証明していている。
置換公理
置換公理は、集合の要素を関数で置き換える。
∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
ここの存在記号は
Replace : OD → (OD → OD ) → OD
という関数で実現する。公理は以下のようになる。
replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ
replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) )
置換公理では置換された元の要素の存在を示す必方がある。否定形の∃をさらにODの形にして使う。
in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD
in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
これを上界とともに要求する。
Replace : OD → (OD → OD ) → OD
Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
恒真性の証明は煩雑なので省略する。
冪集合の公理の恒真性
田中先生の本では以下のように定義されている。
∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
この存在記号は
Power : ( A : OD ) → OD
という関数で消去する。t ⊆ X は record で
record _⊆_ ( A B : OD ) : Set (suc n) where
field
incl : { x : OD } → A ∋ x → B ∋ x
とする。Agda での公理は以下のようになる。
power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
これの恒真性は少し厄介で、部分集合全体を定義する必要がある。まず、部分集合を別な形で定義する。
ZFSubset : (A x : OD ) → OD
ZFSubset A x = record { def = λ y → def A y ∧ def x y }
これは ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) で部分集合とつながっている。
上界は順序数でしか得られないが、その順序数よりも対応する順序数が小さいOD全体というODを定義できる
Ord : ( a : Ordinal ) → OD
Ord a = record { def = λ y → y o< a }
Def : (A : OD ) → OD
Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
これは少し大きすぎるので、これの要素 x を A ∩ x で置き換える(いくつかは空集合になる)と部分集合全体になる。
Power : OD → OD
Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
つまり順序数の冪集合は作るのは簡単なので、それを作って、通常の集合との∩を取るという方針である。
∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
なので、部分集合との∩を取っても問題ない。
順序数 Ord a に対しては冪集合のintroが成立する
ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
これを使って、
power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
を示すことができる。
正則公理、選択公理、ε-induction
正則公理は自分自身と交わらない要素を要求するのだが、それを関数で置き換えてしまうと、集合から必ず要素を取ってくる選択公理と同等になってしまう。つまり、正則性で存在を関数として明示するなら、それは仮定する必要がある。
minimal : (x : OD ) → ¬ (x == od∅ )→ OD x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )そこで、ε-induction ( 任意の集合の要素について成立すれば、全部の集合について成立する)を採用する。これらから、∋の無限下降列が存在しないこと、そして、排中律を仮定すると正則公理が導出できることが証明されるはずである(がやってないです)
ε-induction : { ψ : OD → Set (suc n)}
→ ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
→ (x : OD ) → ψ x
これは順序数とODが対応しているので順序数の TranFiniteInduction そのものになる。
選択公理は田中先生の本のものではなく、Wikipedia にのっているものだと
∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
となっている。これを以下のように定式化する
choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
少し形が異なっているが、 ∅ ∉ X を要求していない分扱いやすい。
選択公理と排中律
ODは順序数と対応するので自明に順序があり、整列定理が成立している。整列定理は選択公理と同等なはずだが、その証明には排中律が必要となる。実際、選択公理から排中律を証明することもできるので、この構成法では、選択公理と排中律は同値な命題となる。
ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p
ppp {p} {a} d = d
によって OD と述語を対応させることできるので、ODの要素を取ってこれるかどうかで p が成立するかどうかを判定できる。ODは空集合かそうでないかどちからなので、p ∨ ( ¬ p ) となる。
ZF内部からはODに対応する順序数を得ることはできないとしないと、整列定理は自明に成立してしまう。
ZF集合論の公理の関係
これらを整理すると以下のような図になる
非構成的な仮定のまとめ
順序数とODの対応
od→ord : OD → Ordinal
ord→od : Ordinal → OD
oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
ODの等号
==→o≡ : { x y : OD } → (x == y) → x ≡ y
上界の存在(最小上界ではない)
sup-o : ( Ordinal → Ordinal ) → Ordinal
sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ
選択公理あるいは強い正則公理
minimal : (x : OD ) → ¬ (x == od∅ )→ OD x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
で、これ正しいの?
ZFの公理は「構文的に教科書に載っているものと同じ」。ただ、否定の位置とかが異なる。
排中律を仮定すると同等になる。
排中律を仮定して直観主義論理は矛盾しないのか? 排中律が証明されるとすると矛盾。仮定なら問題ない。
上界に関係しない部分は単なる論理的な関係
ODと順序数の対応の証明はゲーデル数とかを含むので自明ではない。Agdaで示せるかどうかは不明。
上界に関係する部分は純粋な仮定。順序数の上界がないと自明に矛盾するが、ここでは明示的な制限は入れてない。(少し怪しい)
様々な証明は集合論の議論と平行しているので、まぁ、正しそうな感じ．
Agdaでの集合論の取扱い
record ZF を仮定(つまり入力として)して、そのまま集合論を展開する必要ならば選択公理を仮定する。あるいは排中律を仮定して良い。
非構成的な仮定のみを要求して、理論を展開する。record ZF から非構成的な仮定が導けるかどうかは確認していないので、それで証明されたものが集合論で証明されるとは限らない。
無理して record ZF を使う必然性はない。つまり、Agda で位相空間とかを扱う場合でも集合論が必須なわけではない。
Topos と集合論
Topos は圏論での構造で、Cartesian closed category で subobject classifier を持つもの。Category は自然演繹そのものだが単純に∨と否定を入れると矛盾してしまう。なので直観主義論理のモデルとして使うにはToposを使う必要があるらしい。
Topos にPower Set Functorを入れると集合論になる。ただし、この場合の集合は推移性がないと圏にならない。なので、A ∩ x とるいうここで使った手法を使う。
Oisusによる論文があるがモデル論的な議論になっていて証明論的にもできると書いてある。ここではそれを証明論的に実行したことになっている。
濃度と連続体仮説
濃度を定義にするには選択公理が必要なので排中律を仮定して良い。濃度を定義するには、二つの集合の要素の対応を集合として定義する必要がある(まだやってない)。それから、Filter を定義して(まだやってない)、そのFilter を使ったZF集合論のモデルが連続体仮説を満たさないものを見つけると独立性を示せる(まだやってない)。連続体仮説自体は以下のような命題だと思われる。
continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
Filter
filter は ideal の双対であり、束上の数学的構造である。自然数上の filter の存在は選択公理に依存する。
record Filter ( L : OD ) : Set (suc n) where
field
filter : OD
proper : ¬ ( filter ∋ od∅ )
inL : filter ⊆ L
filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
これを用いて超準解析のモデルや集合論のモデルを作れるはず。
コーエンの方法では集合論の中で直観主義論理を構築して、それと filter を対応させると言う作業が必要だが、Agda 上なら、それらをパスして証明できるかも知れない(まだやってない)。
数学をプログラミングする
数学は Agda 上では、証明を値とする関数型プログラミングだと思って良い。そこで構築される数学的構造は
record と dataであり、データ構造に過ぎない。証明は実際に計算が進むわけではなく、型整合によって確認されるが、そこでは項の正規化は行われる。つまり、再帰呼び出しではない計算は実行されている。
複数の再帰が絡む場合の Agda の型推論は限定的で自明でない。
数学的構造に対応する record を定義するだけでも数学の理解が進む。例えば、
圏論 (米田の補題、随伴関手定理、ApplicativeとMonoidalの関係)
Automaton ( Subset construction、Language containment)
などが Agda によって証明されている
link
数学基礎論サマースクール選択公理と連続体仮説https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/
公理的集合論の基礎 酒井 拓史
https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf
Agda
https://agda.readthedocs.io/en/v2.6.0.1/
ZF-in-Agda sourcd
https://github.com/shinji-kono/zf-in-agda.git
Category theory in Agda source
https://github.com/shinji-kono/category-exercise-in-agda