檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2018-07-30 (月)

全称・存在限量子の色々をまとめた絵

| 15:11 | 全称・存在限量子の色々をまとめた絵を含むブックマーク

過去に、随伴関手対を使った全称限量子と存在限量子の解釈や、限量記号(∀と∃)の使い方などを述べたことがあります。これらのことを、短くまとめる必要があったので、まとめの絵を描きました。その絵をこの記事に載せます。

過去記事

全称限量子と存在限量子に関する過去記事を挙げておきます。本記事は短いまとめなので、より詳しいことを知りたくなったら過去記事を参照してください。

原理的な話は:

実際の証明で限量子をどのように扱うかのノウハウは:

全称限量子のまとめの絵

出現している記号の説明をします。

  • Pred[X] -- 集合X上の述語の集合。述語は、X→{True, False} という関数だと思っても、Xの部分集合だと思っても、どっちでもいいです。述語のあいだの順序関係をもとに、圏とみなします。
  • π2:X×Y→Y という第二射影
  • π2*:Pred[X]→Pred[X×Y] -- 第二射影π2から誘導される述語のあいだの写像。述語を関数だと思うなら、π2*(P) := P¥circπ2 。構文的には、変数水増し〈variable thinning〉オペレータです。
  • '-|' は随伴対を表す記号。

(関手の)随伴対については、次が詳しいです。

ただし、詳しすぎるかも。論理に出てくる随伴対は、プレ順序集合と単調写像における随伴対(ガロア接続)なので、次の記事のほうがお手軽です。

述語論理とプレ順序集合における随伴対(ガロア接続)の関係は、次の記事で主題的に扱っています。

絵の各部の説明
  • 1行目は、π2*:Pred[X]→Pred[X×Y] と ∀:Pred[X×Y]→Pred[X] が随伴対であることを主張しています。
  • その下は、ホムセット同型による随伴対の記述です。
  • その下は、関手の随伴対を図式で表現したものです。
  • 一番下の段は、証明における∀の使い方で、四角い箱は「論理の全称記号∀も存在記号∃もちゃんと使えるようになろう」で説明した∀導入ボックスです。π2*(Q) を Q' と略記しています。Q'(x, y) := Q(y) 。Q'にxは出現しません。

存在限量子のまとめの絵

記号は全称限量子のときと同じです。

絵の各部の説明
  • 1行目は、∃:Pred[X×Y]→Pred[X] と π2*:Pred[X]→Pred[X×Y] が随伴対であることを主張しています。
  • その下は、ホムセット同型による随伴対の記述です。
  • その下は、関手の随伴対を図式で表現したものです。
  • 一番下の段は、証明における∃の使い方で、四角い箱は「論理の存在記号∃をちゃんと使えるようになろう」で説明した∃除去ボックスです。π2*(R) を R' と略記しています。R'(x, y) := R(y) 。R'にxは出現しません。

∀導入と∃除去のボックスと固有変数条件

∀導入でも∃除去ボックスでも、ボックスの先頭で a∈X という変数宣言があります。選言された変数はボックス内でだけ使える変数です。このようなボックス・ローカルな変数を固有変数〈eigenvariable〉とかパラメータと呼ぶことがあります。

固有変数に関する条件〈eigenvariable condition〉をご存知の方、気になる方がいるかも知れません。ボックス -- つまり、変数のブロックスコープをちゃんと使うなら、固有変数条件を気にする必要はありません。

ブロックスコープにおいては、次のようなことは起きません。

  • ブロック外の変数が、ブロック内の同名変数を上書きしてしまう。
  • ブロック内の変数が、ブロック外でも使えてしまう。

ブロックスコープ構造を使ってない場合は、上記のような困った現象が起きるので、それを避けるために固有変数条件を付けています。