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

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

2017-11-24 (金)

存在記号の除去規則について考える

| 14:08 | 存在記号の除去規則について考えるを含むブックマーク

全称記号の導入規則について考える」の続編として、存在記号の除去規則について考えます。

存在記号の除去規則の背景は比較的に簡単な事実です。にも関わらず、記号を換えたり書き方を縦にしたり横にしたりのどうでもいいワチャワチャが事情を見えにくくしています。この記事によって、ワチャワチャな作業(記法のあいだの翻訳)に慣れて、その“どうでもよさ”(記法が変わっても内実は変わらないこと)を感じていただければ幸いです。

内容:

  1. 存在記号の除去規則
  2. 限量随伴性
  3. 引き戻しと存在限量子の随伴性
  4. 随伴性を証明に利用する
  5. 随伴性からサイド証明へ
  6. メタ循環構造

存在記号の除去規則

標準的な自然演繹における「存在記号の除去規則」は次の形に書かれます。

         P(a)
          :
          :
 ∃x.P    Q
 -------------[∃除去]
       Q

僕は、自然演繹に愚痴を言い悪態をついてます(「自然演繹はちっとも自然じゃない -- 圏論による再考」参照)。この規則も、これを見ただけでは何だかよくわかりません。自然演繹ったら、ほんとにもう。

全称記号の導入規則について考える」で、多少マシな形の推論規則が載っている解説"Natural deduction for predicate logic"(https://cs.uwaterloo.ca/~plragde/cs245old/06-prednd.pdf)を紹介しました。"Natural deduction for predicate logic"における全称記号の除去規則は次の形です。

あんまり代わり映えしないですね。でも、右側の証明部分をボックスで囲んでいるのはやっぱりマシです。このボックスで囲まれた部分の証明を、サイド証明〈サブ証明 | 補助証明〉と呼ぶことにします。

サイド証明があるなら、当然にメインの証明があります。メイン証明を左側に、サイド証明を右側に書くようにすると、次のようになります。すぐ上の規則とは記号が違っています; φ→P, x0→a, χ→Q と対応してます。記号の選び方は趣味の問題で、どうでもいいものです。

 メイン証明
   :
 ∃x.P
 -------+-[変数a]--
        | P(a)
        |  :
        | サイド証明
        |  :
        |  Q
 -------+----------
   Q
   :
 メイン証明

このメイン証明とサイド証明の関係をハッキリさせて、存在記号の除去規則の意味付けをします。

限量随伴性

述語論理とインデックス付き圏と限量随伴性」で述べたように、限量子の挙動を支配している原理は随伴性〈adjunction〉*1です。随伴性には色々な表現があります、ホントにウンザリするほど色々な書き方(描き方)があります。表現の多様性が目くらましとなって、単純な本質が見えにくいのです(ため息)。

集合Xごとに、Xの上の“述語”と呼ばれるナニモノカを要素とする集合Pred[X]が対応しているとします。いま「述語」という言葉を使いましたが、代わりに「命題」とか「論理式」とか「文」とか呼んでもかまいません。これらの言葉に合意された定義も識別もありません(人それぞれ、解釈と用法は異なります)*2

呼び名はホントにどうでもよくて、重要な点は、Pred[X]がデカルト閉圏の構造を持つことです。デカルト閉圏が難しそうなら、ハイティング代数やブール代数だと思ってもかまいません。Pred[X]内で、'∧'(連言)、'⊃'(含意)、'|-'(証明可能)などの解釈ができればそれでいいのです。

ここでは、分かりやすい例として、Pred[X]とは“Xベキ集合”のことだとしましょう。つまり Pred[X] = Pow(X) (Pow(X)はXのベキ集合)と置きます。そして:

  • Pow(X)の要素を、「命題」とか「述語」とか呼ぶ。Xの部分集合Aは、p(x) := (if x∈A then True else False) というブール値関数と1:1対応するので、部分集合を述語(あるいは命題)と呼んでも悪くはないでしょう(何と呼ぼうがどうでもいいんだけど)。
  • A, B∈Pow(X) に対して、A∧B は A∩B のことだとする。
  • A, B∈Pow(X) に対して、A⊃B は Ac∪B のことだとする。(-)cは、Xを全体集合としての補集合。
  • A, B∈Pow(X) に対して、A |- B は A⊆B のことだとする。

「ブール値関数←→部分集合」という対応に基づき、論理的演算/論理的関係である ∧, ⊃, |- を、集合の演算/集合の関係 ∩, (-)c∪(-), ⊆ と同一視してしまえ、ってことです。この発想はちょっと乱暴ですが、述語論理(のモデル)のイメージを手っ取り早くつかむには良い方法かと思います。

述語論理とインデックス付き圏と限量随伴性」で述べた一般論では、f:X→Y を写像とすると、f*:Pred[Y]→Pred[X] という逆方向の関手があります。今扱っている Pred[X] = Pow(X) という事例では、f*:Pow(Y)→Pow(X) は、逆像を対応させる写像です。その定義は次のとおり:

  • B⊆Y に対して、f*(B) = {x∈X | f(x)∈B}

f*がベキ集合のブール代数構造に対する準同型写像であることはすぐに分かります。次を確認してください。

  • f*(B∩B') = f*(B)∩f*(B')
  • f*(B∪B') = f*(B)∪f*(B')
  • f*(Bc) = (f*(B))c

包含順序も保存します。

  • B⊆B' ならば、f*(B)⊆f*(B')

さて、f*:Pow(X)→Pow(Y) (星が下付きなのに注意!)は、像〈順像〉を対応させる写像とします。その定義は次のとおり:

  • A⊆X に対して、f*(A) = {y∈Y | x∈A で f(x) = y となるxが存在する}

f*とf*のあいだには次の関係があります。

  • f*(A)⊆B ⇔ A⊆f*(B)

この関係があるとき、f*とf*は、随伴ペアであると言います。随伴ペアであることは、次の2つの包含関係式としても表現できます。

  • A ⊆ f*(f*(A))
  • f*(f*(B)) ⊆ B

詳しくは次の記事を参照してください。

f*とf*の随伴性(随伴ペアであること)が、存在限量子の存在限量子の性格と扱い方を規定します。別な言い方をすると、随伴性が存在限量子の背後にあるメカニズムなのです。

引き戻しと存在限量子の随伴性

f*はfの逆像写像、f*はfの順像写像です。順像写像f*を∃fとも書きます。論理の存在限量子が、事実上順像写像と同じなのでこの記法を使います。

随伴を表すために'-|'という記号を使いますが、次の2つの命題は同じ意味です。

  • f -| f*
  • 任意の A∈Pow(X), B∈Pow(Y) に対して、∃f(A)⊆B ⇔ A⊆f*(B)

そして、次のような言い方をします。

  • fとf*は(この順で)随伴ペアである。
  • fは、f*左随伴パートナーである。
  • f*は、∃f右随伴パートナーである。

逆像写像(逆写像じゃないよ!)f*は、もとの写像fと逆方向に集合を移動するので、引き戻し写像〈pull-back mapping〉とも呼びます。∃fは引き戻し写像の左随伴パートナーで、fと同じ方向に集合を移動します。この∃fを「fの存在限量子」と言ってしまうと混乱を招くかもしれません。「構文的な存在限量子に対応する意味的な存在物」とでも言えば正確でしょう。正確だけど鬱陶しいのでヤッパリ「存在限量子」と呼んじゃうもしれませんね*3

述語論理では、一般的なfに対する ∃f, f* を考えるわけではなくて、π:X×Y→X (射影)という特別な写像だけを考えます。πは、正確に書けば π1X,Y のように上下に添字が付きますが、(x, y) |→ x と1番目の成分を取り出す写像です。(x, y) |→ y (第二射影)を使っても同じことです。

写像 π:X×Y→X に対して、∃πとπ*の随伴性を述べれば:

  • π -| π*
  • 任意の A∈Pow(X×Y), B∈Pow(X) に対して、∃π(A)⊆B ⇔ A⊆π*(B)

この状況を雑に絵に描けば次のようです。この絵を目に焼き付けて続きを呼んでください。

随伴性を証明に利用する

前節で述べた随伴性 ∃π -| π* を意識しながら、存在限量子記号'∃'の扱い方を考えます。ここでは、構文と意味との対応をキッチリとは定義せず、前節で説明した随伴性を頭に置きながら、同様なことを構文的に表現してみよう、という態度で進めます。

まず、構文的な述語〈述語論理の論理式〉をP, Qなどで表します。Pが型Xの変数xを含むかも知れないことを P[x:X] と書きます。型とは、変数が走る集合のことです。Pに、x:X と y:Y という変数が含まれる(かも知れない)ことを表すには P[x:X, y:Y] と書きます。以下、Pは二変数を持ち P[x:X, y:Y]、Qは一変数で Q[x:X] であると仮定します。ここで使った記法に関するより詳しいことは次の記事で説明しています。

X上の変数を持つ述語 Q[x:X] に対して、それを二変数 x:X, y:Y の述語とみなしたものを [x:X, y:Y].P[x:X] と書きます。前置する [x:X, y:Y]. は変数水増しオペレーター〈variable thinning operator〉です。変数水増しオペレーターは、射影 π:X×Y→X による引き戻しπ*:Pow(Y)→Pow(X) に対応する構文的オペレーターです。

述語〈述語論理の論理式〉に対する存在限量子は、普通に ∃w:Y.P[x:X, w:Y] と書きます。束縛変数は何を使ってもいいのですが、主に w:Y を使います。

以上に述べた構文的な構成と、前節の部分集合/ベキ集合との対応をまとめると以下のようです。

部分集合/ベキ集合 述語論理
A∈P(X×Y) P[x:X, y:Y]
B∈P(X) Q[x:X]
π*:Pow(X)→Pow(X×Y) [x:X, y:Y]. 変数水増し
π*(B)∈Pow(X×Y) [x:X, y:Y].Q[x:X]
π:Pow(X×Y)→Pow(X) ∃w:Y. 存在限量子
π(A)∈Pow(X) ∃w:Y.P[x:X, w:Y]

この対応をもとに、随伴性を述語論理の言葉で表現してみます。随伴性をもう一度繰り返し書くと:

  • π(A)⊆B ⇔ A⊆π*(B)

左右に並べる代わりに上下に書くと:

π(A)⊆B ⇒ A⊆π*(B) を上下に書く:

   ∃π(A)⊆B
 -------------
   A⊆π*(B)

A⊆π*(B) ⇒ ∃π(A)⊆B を上下に書く:

   A⊆π*(B)
 -------------
   ∃π(A)⊆B

このように上下に並べる書き方は、論理の話ではよく使われます。上の対応表を見ながら、また'⊆'を'|-'に直して書き換えると:

   ∃w:Y.P[x:X, w:Y] |- Q[x:X]
 ------------------------------------
   P[x:X, y:Y] |- [x:X, y:Y].Q[x:X]


   P[x:X, y:Y] |- [x:X, y:Y].Q[x:X]
 ------------------------------------
   ∃w:Y.P[x:X, w:Y] |- Q[x:X]

これが何を主張しているのかと言うと:

  • 「∃w:Y.P[x:X, w:Y] を仮定して Q[x:X] が証明できること」と「P[x:X, y:Y] を仮定して [x:X, y:Y].Q[x:X] が証明できること」は同じである。

ちょっと言い方を変えると:

  • ∃w:Y.P[x:X, w:Y] を仮定して Q[x:X] を証明したいなら、P[x:X, y:Y] を仮定して [x:X, y:Y].Q[x:X] を証明しても(同じことだから)よい。

随伴性からサイド証明へ

いよいよ大詰めですが、時間に余裕がある方は、次の記事の冒頭と最初の節、最後の節を読んでみてください。

我々が何かを学ぶとき、記法に慣れるのに相当な労力が割かれます。同じ内容であっても、異なる記法で提示されると理解できません。異なる記法のあいだの翻訳にも手間がかかります。論理式や証明の書き方(記法)も色々あって、それらの翻訳でけっこう消耗してしまうことがあります。残念ながらどうにもならないので、記法の変更(書き換え、翻訳)に慣れるしか無いです。

この記事での縦と横の描き換えを体験すれば、僕がたまにしている「双対や随伴に強くなるためのトレーニング」が、冗談でないことが分かるでしょう。

さて、随伴性の表現に対して、'⇒'を使った横書きを横線区切りを使った縦書き(上段と下段を使用)にしました。さらにまた90度回転して書きます。

                  |
∃w:Y.P[x:X, w:Y] |  P[x:X, y:Y]
   ---            |     ---
    |             |      |
                  |
  Q[x:X]          |  [x:X, y:Y].Q[x:X]
                  |

“左側上下の証明可能性”と“右側上下の証明可能性”が同等であることを主張しています。内容的には前節とまったく同じですが、レイアウトが変わっています。

新しいレイアウトに沿って説明すると、左上から左下に至る証明をすることは、右上から右下に至る証明をすることと同等なのです。であるならば、左上から左下への証明はやらずに、右上から右下をやるだけでいいはずです。

もう一度図を描きかえて、事情を分かりやすくします。

      :               |
      :               |
(1) ∃w:Y.P[x:X, w:Y] |
                      |(2) P[x:X, y:Y]
                      |      :
                      |      :
                      |(3) [x:X, y:Y].Q[x:X]
(4) Q[x:X]            |
      :               |
      :               |

左側の証明記述が論理式(1)(存在命題)に到着したとき、(4)に至る経路として、いったん右の論理式(2)に移り、そこで証明をして論理式(3)に至り、そこで再び左側(4)に移って証明を続ければいいのです。

上記のレイアウトにおいては、左側がメイン証明が進行するレーン、右側がサイド証明〈サブ証明 | 補助証明〉が進行するレーンです。右側レーンは、いつも必要なわけではなく一時的なので、一時的に出現するボックスと考えてもいいでしょう。

      :
      :
(1) ∃w:Y.P[x:X, w:Y] +---------------------
                      |(2) P[x:X, y:Y]
                      |      :
                      |      :
                      |(3) [x:X, y:Y].Q[x:X]
(4) Q[x:X]            +----------------------
      :
      :

メイン証明は集合X上の証明、ボックス内のサイド証明はX×Y上の証明となっており、証明の舞台が異なります。その意味でも、メイン証明とサイド証明はしっかり区別したほうがいいのです。"Natural deduction for predicate logic"の記法(書き方/描き方)がマシなのは、サイド証明をちゃんとボックスで識別している点です。

紙面の節約のために、右側のボックスを左に押し込んでしまいます。ボックスの入り口と出口の区切り線は残します。(1)から(2)に移るときに束縛変数を自由変数に置き換えますが、これはどんな変数でもかまいませんが書き添えておくことにします。さらに、[x:X, y:Y].Q[x:X]とQ[x:X]を通常は区別しないので、変数水増しオペレーターは省略してしまうと:

      :
      :
(1) ∃w:Y.P[x:X, w:Y]
   +--[変数 b]------
  (2) P[x:X, b:Y]
        :
        :
  (3) Q[x:X]
   +----------------
(4) Q[x:X]
      :
      :

サイド証明ボックス内で使う変数は、ボックスの入り口で宣言しています。この変数の選び方は本来まったく自由ですが、それまで出現してない変数(フレッシュ変数)を選んで混乱を避けるのが普通です。

ここでまた愚痴と悪態を吐くと; 証明の書き方では、変数のブロックスコーピングを導入せずに、フラットスコープとフレッシュ変数を使うことが多いのですが、このやり方だと変数が増大してロクなもんじゃないです*4

メタ循環構造

ここまでの話で、存在限量子の背後には次の随伴性があることを説明しました(f*と∃fは同じ意味です)。

  • [随伴性] f*(A)⊆B ⇔ A⊆f*(B)

この随伴性は、次の2つの包含関係式と同値です(「順序随伴性: ガロア接続の圏論」参照)。

  • [単位関係式] A ⊆ f*(f*(A))
  • [余単位関係式] f*(f*(B)) ⊆ B

実は、「証明の“お膳立て”のやり方 オマケ1: 集合の内包的記法の困惑」の例題は二番目の関係式(余単位関係式)でした。少しサボった記法で次のように書いていました。

  • f(f-1(B)) ⊆ B

余単位関係式の証明には、今回説明した存在限量子の除去規則を使います。「証明の“お膳立て”のやり方 オマケ1: 集合の内包的記法の困惑」の最後のほうでゴニョゴニョ説明していることは、実質的には存在限量子の除去なのです。

存在限量子の除去規則の根拠は随伴性だと言い、その随伴性の証明には存在限量子の除去規則を使う … これって循環論法ではないのか?

たしかに循環しています。しかし、このような循環はしばしば出会うものです。我々が生きているこの世界で成立していると信じられている法則、ずっと使われ続けている手順などを、我々が構成・操作・調査できるモデルのなかで再構成し合理化することは意義があるのです。

このような循環が起きる状況には“入れ子の世界”が介在しています。“入れ子の世界”はミステリアスで、人を不安にさせるかも知れません。が、“入れ子の世界”とそれに伴うメタ循環〈メタ巡回 | meta-circlular〉構造は避けられないのです。次の記事も参照してください。

*1:随伴性は、双対対象ペア、随伴関手ペアを含む一般的な概念ですが、ここでは随伴関手ペアの意味です。

*2:もちろん、特定の文脈では定義され、識別もされます。

*3:世間一般に、不正確さや混乱のリスクがあっても、簡略な用語法・記号法を採用する傾向があります。面倒なのは嫌なんですが、こういう簡略さが、理解をおおいに阻害しているのも事実です。ほんとに頭が痛いところです。

*4プログラミング言語で、大域変数しかないものを想像してもらえれば、酷さが分かると思います。