Extensional axiom of choice という公理があるらしい
二年前に 直観主義と選択公理の話 という記事を書いたのですが,それに近い内容の論文を 2006 年に Martin-Löf が書いていたこと知りました。"100 Years of Zermelo’s Axiom of Choice: What was the Problem with It?" というタイトルの論文で,Springer から出版されています (http://link.springer.com/chapter/10.1007%2F978-1-4020-8926-8_10) が,同じ内容と思われる(確認してないけど) pdf が https://people.kth.se/~kurlberg/colloquium/2005/MartinLooef.pdf で公開されています。
この論文は,どうして選択公理は BHK 解釈のもとでは自然に成立するように思えるのに排中律を導くという非構成的性質を持つのか,ということを論じたもので,結論は「関数の存在はいえても,その外延性が保証できない,つまり等しい値に対して等しい結果を返すことが証明できないから」ということで上記の記事と一致しているようです。
Extensional axiom of choice
その論文中で導入されている extensional axiom of choice (ExtAC) という公理が面白かったので,それについて議論されていることをまとめておきます。技術的詳細には立ち入りません,というか以下の議論が正確にはどう形式化できるのかよく理解できてない部分があります。しかし詳細がわからなくても informal な説明としてはそれらしいものであると思います。
ExtAC は,普通の集合論の中ではただの AC と区別がつかないのですが,構成的型理論 (CTT) の中で考えると AC と同値ではない公理です。この ExtAC と AC の差を観察することで選択公理が成り立つ集合論が非構成的になる理由がわかる,という点が面白いところです。
ExtAC を考えるための前提として,型における等しさの概念は型そのものの定義とは別に与えられると考えることに注意が必要です。CIC のように inductive type をもつ型理論では identity type は一様に定義できますし,Martin-Löf 流の型理論でも同様のやり方で導入することができますが(propositional equality と呼んだりする),それとは別に等しさを考えるということです。別の言い方をすると,ただの型ではなく setoid を考えるということです。
いま I と S を型とし,その上の等しさが与えられたとして,それらを各々 , と書くことにしましょう。これらの等号については,それぞれ I と S の上の同値関係であることしか仮定しません。また,以下 A は 上の述語でこれらの等号を respect する(つまり かつ なら である)ものとします。
まず,通常の選択公理 AC は
となります。これは等しさに言及しないバージョンで,この形のものは CTT で証明できるのでした。ただし, だからといって かどうかはわからないことに注意しましょう。等号は任意に与えた同値関係としたのだから,確かに CTT における AC の証明はこれを満たす f を与えるとは限らないでしょう。
ExtAC は以下のように定式化されます。
ただし Ext(f) は f が外延的であることを表す述語で,次のように定義されます。
また,正確には一番外側に を束縛する全称量化子(とそれらに関する諸々の条件)が付くと思いますが省略しています。
AC と違って,ExtAC は CTT では証明できません。論文中では,実は ZFC から CTT + ExtAC への翻訳が存在することが示されています("ZFC is interpretable in CTT + ExtAC" と書いてありますが,そういうことでしょう)。ということは,ラフな言い方をすると,集合論的な意味での AC に相当する型理論の公理は AC ではなく ExtAC であることがわかります。
証明の詳細をきちんと確かめていないのですが,だいたいどういうことかというと,集合論では集合の商をとることができるのがポイントになっているようです。このことは,与えられた同値関係の意味での同値性を,集合としての等しさに置き換えることができるということを意味します。もし述語 A が与えられた同値関係を保てば,A は商集合の上の述語としても well-defined ですから,先に商をとったうえで AC を使うことで ExtAC 相当のことができるのでしょう。
補足しておくと,通常の集合論においては等しさの概念は論理に組み込まれているものを使いますから,どんな関数も等しさを保存するということは集合論がその上に乗っているところの一階述語論理のレベルで保証されています。したがって,そもそも外延的でない関数など存在するはずがないので,Ext(f) は恒真であり,そのような述語は何を言っていないのと同じです。だから当然,ExtAC 相当のものを集合論で考えても,それはただの AC と同値です。したがって両者は集合論においては区別できません。
このように AC と ExtAC を区別したうえで議論をすると,集合論において選択公理がどのようにして構成的でない結論を導いているのかが見えやすくなります。両者の差は Ext(f) を要求するかどうかにあるわけだから,その違いが効いているということです。つまり Ext(f) を満たすような f を構成的に与えることはできないのです。これで最初に述べたように,選択関数が作れないのは選択できないからではなく外延性が保証できないからである,という結論に到達しました。
二年前の記事では同じ事情を「多価でもよいなら選択関数は存在する」という形で表現したのですが,今回紹介した Martin-Löf の議論はその別表現と言うことができるでしょう。
*1:ここでは量化子は他の結合子よりも強く結合することにします
世界が 11 次元だとすると重箱の隅は 1024 個もあるのでつつき放題
何がきっかけか忘れたのですが,一般に n 次元の重箱には隅が 2^(n-1) 個あるのだなということを思ったので,たいした話ではありませんが書いてみることにしました。
n 次元重箱とは,n 次元立方体の境界から一つの側面の内部を除いた図形である。具体的には,例えば の点であって少なくとも一つの座標が 0 または 1 である点の集まりから,第 n 座標のみが 1 であるような点をすべて除いてできると考えてよい。その場合,重箱の隅とは,第 n 座標が 0 であり,その他のすべての座標が 0 または 1 であるような点のことである。
そうすると,隅の集合は だから 個ある。だから例えば通常の 3 次元重箱には隅が 4 個あり(これはわれわれがよく知っている重箱の隅の個数と一致する),11 次元なら 1024 個ある。
数遊び
ある日の夜,寝ようとして布団に入った瞬間に,どういうわけか 676 という数字が浮かんできた。
見覚えのある数字だ。でもどこで見たのだろうか。平方数か何かだろうか。そういえば 24 の二乗はそんな感じの数だった気がする。そこで計算してみると ,ちょっと違う。
試しに素因数分解でもしてみようと思う。676 = 700 - 20 - 4 で右辺に出てくるのは 4 の倍数だから,676 は 4 で割り切れる。そこで試しに割ってみると 676 = 4 * 169 となる。169 は知っている。13 の二乗である。
ということは なのか。そういえばそうだったような気がする。
そうすると 576 と 676 はいずれも平方数なのだ。そんなことがあるだろうか?というのは,平方数は疎らにしか存在しないように思えるので,両者の間隔がちょうど 100 というきりのいい数になるということはそれほどありそうにない。*1
それではなぜ なのか。計算してみればそうなる,というのは論理的に正しいが,論理的に正しい証明が必ずしも納得をもたらすわけではない。
そういえば,24 と 26 の間には 25 があり,100 は 25 の倍数である。たぶんここから何かわかるのではないか。
平方数が奇数の和であることを思い出そう。つまり である。そうすると と がわかるから(これは を使っても確かめられる),確かに でなければならないとわかった。少し納得した。
こんなことを考えているから眠れない。
掛け算の順序を区別するなら割り算は二つ必要
掛け算記号の左右の役割は異なるので順番を入れ換えてはいけないという立場がある。左側は「一単位あたりいくつ」を表し,右側は「何単位分あるか」を表すのであり,それらを逆に書いてはいけないのだという。例えば,2×3=6 と書いたらそれは「三人がそれぞれ二つずつみかんを食べた」という状況は表すが「二人がそれぞれ三つずつみかんを食べた」という状況は表さない,ということだと理解している。
その立場を貫こうとすると,掛け算記号の左側を求めるための割り算と右側を求めるための割り算の二つが別々のものとして導入されねばならないように思う。2×3 と 3×2 で意味が異なるのだったら,□×3=6 と 2×□=6 のそれぞれにおいて □ に入る値を求めようとするとき,両者において用いられるべき演算が同じである理由はない。□ はそれぞれ異なる役割を担う位置に置かれているのだから,それを求めるのにも異なる演算が用いられると考えるのは道理であるし,実は同じ演算で求まるのですと言われてもそう簡単に納得できるようには思えない。実際それらを区別する用語はあって,前者を等分除,後者を包含除と呼ぶ。
しかし,両者を概念として区別することはあっても,例えば異なる記号で表すなど,構文的に区別しているのを見たことはない。これはどうしてだろうか。掛け算の左右を区別するのと同じように,二つの割り算も構文的に区別するべきではないか。そうしないと混乱の元であるのに,横着をして両者をごっちゃにしてはいけない。
というわけだから,□×3=6 の □ を求めるための演算と,2×□=6 の □ を求めるための演算を区別するために,いま仮に前者であるところの等分除を/で表し,後者であるところの包含除を\で表すことにすれば
□×3=6 ⇔ □=6/3
であり,また
2×□=6 ⇔ □=2\6
のように書くことができる。こうすれば見た目にも別々の演算であることが明らかで,わかりやすいのではないか。
最後に参考文献をひとつ挙げておこう。
- 作者: Nikolaos Galatos,Peter Jipsen,Tomasz Kowalski,Hiroakira Ono
- 出版社/メーカー: Elsevier Science
- 発売日: 2007/04/25
- メディア: Kindle版
- この商品を含むブログを見る
Coq 8.5 を入れてみた
先日 Coq 8.5 がリリースされたので入れてみた話。
coq 自体のコンパイルは問題なくできたけど,その後 ssreflect のコンパイルに失敗した。make すると
Error: The files /usr/local/lib/coq/parsing/pcoq.cmi and /usr/local/lib/coq/lib/compat.cmi make inconsistent assumptions over interface Compat
と言われる。問題の compat.cmi はタイムスタンプを見ると Coq の前のバージョンのものらしいことがわかる。どうもソースコードのディレクトリ構成が変わっているようで,新しい compat.cmi は別のディレクトリに存在している。それで Coq を make install したときに上書きされずに古いものが残って,何らかの理由でそれが間違って参照されているようだ。
試しに
sudo rm -fr /usr/local/lib/coq/
してから coq をインストールし直してみると,今度は ssreflect の make に成功した。
mathcomp もコンパイルし直さないといけない。試しに make -j16 とかやってみたら 20 分ちょっとでコンパイルが終わった。
風呂場でする遊び
さっきシャワーを浴びながら考えていたことなど。
8 って 9 - 1 だから平方数(以下,平方数に 0 は含めないことにする)の差だなーということをまず思った。なんで 8 のことを考えていたかは省略する。というかよく覚えていない。
平方数の差はたくさんあるので,これだけだとそんなに面白くない。もうちょっと強い条件はなにか考えられないだろうか。
例えば平方数の差で表せる正の数の中で 8 はどれくらいの位置にいるだろうか。そういう数の中で一番小さいのは 3 である。その次は 5 である。その次ぐらいじゃないか?と思ったが,よく考えたら 7 = 16 - 9 だから違った。
しかし以上のことから,平方数の差で表せる正の数のうち平方数の差で表せる最小の数番目に小さい数は 7 であることがわかった。8 はその次。
7 までに現れる数はすべて奇数だったので,8 の特徴付けとして「平方数の差で表せる最小の正の偶数」というものが考えられることもわかる。
考えてみれば 3 以上の奇数は必ず平方数の差で表せるのだった。そして偶数が平方数の差になることは,それが 4 の倍数かつ 4 より大きいことと同値である。いずれも証明は難しくないので読者への演習問題とする。
ssreflect の proof script のインデント
ssreflect を使っているとき,proofgeneral のデフォルトのままだと(といっても何が本当にデフォルトなのか把握できていませんが,少なくともそんなにいじってないはずの手元の環境では)インデントがあんまりうまくいってない感じが強いので何とかできないかなと思っています。
今日ちょっと coq-smie-indent.el などを見てみたら,by のインデントの調整くらいはすぐにできそうな気がしたのでやってみました。
(defadvice coq-smie-rules (around ssr-by-tactical (kind token) activate) (if (and (eq kind :before) (equal token "by") (save-excursion (skip-chars-backward "\t\n\r ") (= (char-before (point)) ?.))) (smie-rule-parent) ad-do-it))
by はデフォルトではインデントを深くするので,例えば
have -> : 1 + 1 = 2 by reflexivity.
みたいになります。これはいいのですが,ssreflect では by を先頭に書くこともあって,例えば手元にある適当なコードを貼り付けますが
case. move => H; move : (eq_sigT_snd H). by rewrite eq_axiomK.
のようにも書きます。こういうときはインデントを深くしてほしくないので,advice でむりやりそうなるようにしました。
あとは => が tactical (と呼ぶのが正しいのかどうかいまいちわからないけど他に適切そうな言葉を知らない)として使われるときには ; より結合力が弱いはずなんだけどそういう動作になってないようです。
例えば,また適当に手元にあったものを貼り付けますが
by move => H; move : H inv HPinv HVinv inv_env pweq; elim => // *; match goal with [H : _ |- _] => case : H => ? ? ?; subst; eauto end.
みたいなのはデフォルトの動作だと
by move => H; move : H inv HPinv HVinv inv_env pweq; elim => // *; match goal with [H : _ |- _] => case : H => ? ? ?; subst; eauto end.
となってとても残念。
これも何とかできるとよいなと思うのですが,こっちはたぶん文法規則を書き直す必要があるのでもっと面倒そう。