直観主義論理の入り口~Heyting 代数~(その 8)
今回は Heyting 代数の性質についてもう少し詳し見ていきます. 以下 は Heyting 代数とし, とします.
1.
より明らか.
2. ならば
より.
3.
函手 が極限を保つことから従う.
4.
と から
により
よって
分配圏の性質としても導くことができる.
5.
と から従う.
6.
と から従う.
7.
圏論の冪の性質から従う.
直観主義論理の入り口~Heyting 代数~(その 7)
今回は Boole 代数に関する大事な性質について見ていきます.
Boole 代数ではない Heyting 代数が存在する
補題 を Heyting 代数とする. もし に対してその補元が存在するならば, それは擬補元 である.
(証明)
を の補元とする. このとき であるから である. よって単調性により
であるから は定義より直ちにわかるから, も の補元である. は分配的だから, 補元は存在すれば一意である. 故に
を, 通常の大小関係を入れて順序集合と見ると, これは有界束になっています. このとき は
で は
です. そして については
が成り立ちます. よって擬補元については以下の表のようになります.
が Boole 代数になるためには擬補元が補元に一致する必要がありますが, においては
なので, は Boole 代数ではありません. しかし Heyting 代数ではあるので, これは Boole 代数ではない Heyting 代数の例になっています.
直観主義論理の入り口~Heyting 代数~(その 6)
前回まで束に関する一般的な性質を見てきましたが, 今回からいよいよ Heyting 代数の話をします.
Heyting 代数の定義
は有界束とします. このとき が Heyting 代数であるとは, が圏*1として冪を持つことを言います. すなわち函手
が右随伴函手
を持つことを言います.
このとき, 圏の一般論から が余極限を保つこと, 特に
が成り立つので, は分配束であることが分かります.
に関しては
かつ
で特徴づけることができます. つまり圏の言葉を使わずに定義するならば, 有界束 は
に常に最大元が存在するときに Heyting 代数であるといい, のことを と書きます. これを の に対する相対擬補元と言います.
特に の に対する相対擬補元 を単に擬補元と言い, と書きます.
Boole 代数
Heyting 代数の性質を細かく見る前に, Heyting 代数より真に強い概念*2である Boole 代数について見ていきたいと思います.
相補律
有界束 が相補律を満たすとは, 任意の に対して
を満たす が存在することを言います. このとき は の補元であると言います. 一般には補元は一意ではありません. 相補律は自己双対な概念です.
Boole 代数
有界束 が分配束でかつ相補律を満たすとき, は Boole 代数(もしくは Boole 束)であると言います. Boole 代数においては, がともに の補元ならば
が成り立ち, 同様に も示せますので, が成り立ちます. すなわち, 補元は一意に決まります. したがって, Boole 代数では の補元を と書くのが習わしです.
の補元の一意性から が成り立ちます. つまりある元を補元に移すという写像は対合になっています.
de Morgan の法則
は de Morgan の法則として有名です. 証明は
もう一方はその双対です.
ならば なので de Morgan の法則により
が成り立つので が成り立ちます. つまり, 補元を取るという操作は順序を逆にします.
直交相補束
有限次元ベクトル空間 の部分空間の全体は有界束になります. と を部分空間とするとき, 結びは , 交わりは になります.
が の補元であることは と表せますが, 一般に補元は一意でないことは次のような例を考えるとわかります.
とおくと, 明らかに ですが, 一方で任意の は
と表すことができ, また なので も成り立ちます.
しかし, に内積を与えたとき, に対して
とおけば
が成り立ちます.
このことを一般化して, 有界束 について が
を満たしているとき, を直交相補束と言います. 一般に有界束 の直交相補束としての構造は複数入る可能性があります(上記の例では, 内積の取り方によって異なる直交相補束としての構造が考えられる).
直交相補束においては
であり, ならば だから であり, よって であるから が成り立ちます. 同様に も成り立ちます(de Morgan の法則).
Boole 代数は明らかに直交相補束です.
直観主義論理の入り口~Heyting 代数~(その 5)
ある方から証明を教えていただくことができた(正確には証明が載っている書籍を紹介していただいた)ので, 前回あいまいにしていた部分を消化しておきます.
定理. が分配束でなければ
を満たす が存在する.
(証明)
1. がモジュラー束でないとき
このとき かつ を満たす が存在する. 明らかに
が成り立っており, 単調性から
故
と
故
が成り立つ. 従って
が条件を満たす.
2. がモジュラー束のとき
仮定により を満たす が存在する.
と置くと
ここに と から
同様にして
双対で
このことから, のうちいずれか二つが等しければ
となり仮定に反するから, は互いに異なる元であり, これが定理の条件を満たす.
直観主義論理の入り口~Heyting 代数~(その 4)
束についてもう少し
一般の束に関する性質をもう少し見ていきましょう.
が成り立ちます(単調性).
これは
と からわかります.
また
… (*)
が成り立ちます. これは定義に従って地道に示せますので, 証明は省略します.
(*) 式から が導かれます. このことと単調性を上手く使うと
が示せます. (*) 式は自己双対ですが, 上の二式は互いに双対な式になっています. 逆にこの二式から (*) 式を示すこともできるので, この二式を合わせたものは (*) 式と同値です.
直観主義論理の入り口~Heyting 代数~(その 3)
圏としての束
もう少し束の話を続けたいのですが, 圏論の知識を持っているといろいろと楽なことが多いので, 束を圏とみなす方法を紹介します.
一般に束 はそれ自体半順序集合です. これを圏とみなすためには以下のようにします.
- 圏 の対象は の元.
- 圏 の対象 の間の射は
- 射 と射 に対して合成を で定義.
このとき が束であることと, が常に 2 個の対象の余積と積を持つことと同値です. 余積は交わり, 積は結びに相当します. また, が有界束であることは が(余積と積に加えて)始対象と終対象を持つことと同値です. 始対象は最小元 で終対象は最大元 になります. さらに, が完備束であることは が無限余積と無限積を持つことと同値です.
双対圏(逆圏)
一般に圏 が与えられたとき, その双対圏 が定義できます. の対象は の対象で, 射は において であるとき であるとします.
このとき, 例えば が始対象を持つならば、それは における終対象になっていますが, このような関係にある概念は互いに双対概念であると言います.
束を圏とみなしたとき, 交わりと結び, 最小元と最大元は互いに双対概念になっています. また, 束の命題について, その順序関係を逆にし, なおかつ交わりと結びを入れ替えたものが双対命題になっています. 束の双対はまた束なので, 束である命題が成り立つならば, その双対命題も成り立つことが分かります.
直観主義論理の入り口~Heyting 代数~(その 2)
有界束と完備束
有界束
束 は自然な方法で半順序集合とみなせることは前回分かりました. そうなると最小元や最大元は存在するのか, は自然な興味の対象になりますし, 当然ながら常に存在するとは限りません.
最小元と最大元がともに存在する束を有界束と言います. 束の場合は最小元は で, 最大元は で表すのが習わしです. 最小元と最大元については以下が成り立ちます.
証明はいずれも簡単なので省略します. 逆に代数的に定義した束 で, 上記の性質を満たす と があれば, が最小元, が最大元になります.
ちなみに最小元も最大元も存在すれば順序の意味では当然一意に定まりますが, 例えば の他に で を満たすものがあったとすれば
となり, そのような元は代数的にも一意に定まります.
さて, の空でない任意の有限部分集合 については交わりと結び
が自然に定義できます( のときは と約束する). なおかつ の空でない有限部分集合 については
が成り立つのですが, 仮に とすると
という式が出てきます.
気分としては は
を満たすようなものですから, 記号論理の知識がある人ならこれは
を満たすものでなければならないことがわかるでしょう. つまり は の最小元でなければならないのです. 同様に なるものが存在すれば, それは最大元でなければならないはずです. そこで, 有界束においては
とすることで上記の式の整合性が保たれます. 逆に空集合も含めた任意の有限部分集合に交わりと結びが存在するような束は有界束となります.
完備束
ここまでは有限部分集合のみに話を絞っていましたが, 有限とは限らない一般の の部分集合 に対して (交わり)であるということを
を満たすものとして定義します. 順序集合的に言えば ということです. 結びの定義も同様で, 順序集合的には になります.
もちろん, どちらも一般的には存在しないのですが, これが必ず存在するような束を完備束と言います. 完備束 には明らかに最小元 と最大元 が存在するので, 完備束は常に有界束です.
実は完備束においては, 「交わりと最小元」か「結びと最大元」のどちらか一方の存在を仮定すれば, もう一方が定義できます. 例えば交わりと最小元が常に存在するとして, 結びは
*1
で定義します. この式の右辺を と置くとき, 任意の に対して なので が導かれます. *2