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

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

過去記事

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

原理的な話は：

• 全称記号の導入規則について考える
• 存在記号の除去規則について考える

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

• 論理の存在記号∃をちゃんと使えるようになろう
• 論理の全称記号∀も存在記号∃もちゃんと使えるようになろう

全称限量子のまとめの絵

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

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

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

• 圏論の随伴をちゃんと抑えよう

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

• 順序随伴性： ガロア接続の圏論

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

• 述語論理とインデックス付き圏と限量随伴性

絵の各部の説明

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

存在限量子のまとめの絵

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

絵の各部の説明

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

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

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

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

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

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

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