resolution の完全性についての疑問

一階述語論理の resolution の規則って, l \in C, \neg l' \in C' として  \theta l, l' の MGU としたときに
 C, C' \vdash (C\theta \setminus \{l\theta\}) \cup (C'\theta \setminus\{\neg l \theta\})
と書けて(resolution に  \vdash を使うのはあまり普通ではないかもしれないけど),これだけで反駁完全なのだと思っていました。しかしどうもそうではないようだという気がしてきて,どうやったら本当に完全になるんだろうかということを最近考えました。

まず完全でないと思う理由ですが,例えば  \{ \{p(x), p(y)\}, \{ \neg p(u), \neg p(v) \} \} (p は述語記号,x, y, u, v は変数)という節集合を考えます。これが充足不能なのは,論理式で書くと  (\forall x y. p(x) \lor p(y)) \land (\forall u v. \neg p(u) \lor \neg p(v)) だから明らかでしょう。一方,この節集合からは上の規則を使っても  \{ p(z), \neg p(w) \} しか(変数の名前の違いを除いて)新しい節は出てきません。だから空節を導くことはできません。

いくつか見てみた本の中で「論理と計算のしくみ」では違う規則を採用していて,この本では一つずつではなく複数リテラルをまとめて取り出して unify してよいことになっています。具体的には  \theta C' \cup D' の MGU として
 C \cup C', D \cup \neg D' \vdash (C \cup D)\theta
のようにしています。これだとさっきの例は  p(x), p(y), p(u), p(v) をまとめて unify してやれば空節が出てくるので OK,ということになります。この形の規則だと確かに反駁完全性が成り立つようです。

でもそういう形の規則になっている本は他に見かけないので,これはどういうことだろうかと疑問に思い調べてみました。以下の記述は "Handbook of Automated Reasoning" の Chapter 2 の冒頭(を読んだ記憶)に基づいています。どうやら resolution の手法を最初に考えた Robinson は,確かに最初の形を resolution として定式化していたようですが,それに加えて別にもう一つ規則を用意していたらしいです。その規則は factoring といって, \theta を D の unifier として
  C \cup D \vdash (C \cup D)\theta
という形をしています(たぶん)。これがあると,
 \{ \{p(x), p(y)\}, \{ \neg p(u), \neg p(v) \} \} \vdash \{ \{p(x)\}, \{ \neg p(u) \} \}
なので,最初の形の resolution と合わせて空節が導けます。厳密には確かめていませんが,こちらも反駁完全性が成り立ちそうです。

ということは,もともとは resolution と factoring を合わせて反駁完全であるという話だったのに,factoring の方は何らかの理由であまり教科書に書かれなくなってしまったのでしょうか(実際,handbook を読むまで factoring という名前を知らなかった)。https://en.wikipedia.org/wiki/Resolution_(logic) には "The resolution rule, as defined by Robinson, also incorporated factoring, .... The resulting inference rule is refutation-complete, ...." と書いてあるので,そんなに知られていない事実でもなくて,たまたま僕がそのあたりのことが書いてある教科書を読まなかっただけかもしれませんが。

ダウンロードしてみた本リスト

先日 Springer でいろいろな本が無料ダウンロードできるようになっていた。今はもうできなくなったらしい。どういうことだったのかはよく分からない。twitter を見ても,よく分からないと言っている人がたくさんいる。

何冊か落としたのでメモ。

  • Marker, Model Theory
  • Mac Lane, Categories for the Working Mathematician
  • Jech, Set Theory
  • Mac Lane & Moerdijk, Sheaves in Geometry and Logic
  • Cox et al., Ideals, Varieties and Algorithms
  • Hartshorne, Algebraic Geometry
  • Halmos, Finite Dimensional Vector Spaces
  • Shafarevich, Basic Algebraic Geometry 1, 2
  • Fulton, Algebraic Topology
  • van Dalen, Logic and Structure
  • Poizat, A Course in Model Theory
  • Marcja & Toffalori, A Guide to Classical and Modern Models Theory

contraction がいらないシーケント計算

「論理と計算のしくみ」を読んでいたら,シーケント計算の推論規則を

  • ∧右,∨左,⊃左は additive
  • ∧左,∨右 は multiplicative

にすると命題論理では contraction が不要になるということを知りました。こういう組み合わせは証明論的にはだいぶ気持ち悪いような気がしますが,Wang's algorithm に対応するように推論規則を作るとこうなるようです。

一階述語論理では反例があって, \exists x ( (P(a) \land P(b) ) \lor \neg P(x) ) は contraction がないと証明できないようです。∃右規則を

 \displaystyle{ \frac{\Gamma \Rightarrow \Delta, A[t_1], \dots, A[t_n]}{\Gamma \Rightarrow \Delta, \exists xA[x]} }

として,∀左も同様に変更すると contraction なしで済みそうですが(確認してないけど)。

これは一体,何を意味するのだろうか。

Awodey 本の訳に変なとこがある

Awodey 本の邦訳について,訳の質が低いという趣旨のレビューがついています。自分で確認したわけではないのですが,このレビュアーの書いていることを信じるならば,確かにあまり丁寧に訳されてはいないようだという印象は受けます。そこに挙げられている点が数学書の翻訳の質を評価する上で重要かどうかはともかく。

そのレビューに対して「数学的な誤りがあると言うが,具体的にどこにあるのか?」というコメントが付いているのを見て,以前眺めたときにおかしな箇所があったことを思い出しました。それでちょっと確認してみたらやっぱりおかしいようなので,とりあえずここに書いてみます。正確には誤りというか,そもそも意味がわからない文が書いてあるということですが,いずれにしても数学の技術的内容に関わることです。

問題の箇所は注意 9.36 にあります。「A を局所スモール完備圏とし,次の条件をみたしているとする」*1として,二つの条件を挙げていますが,その一つ目が次のようになっています。

1.  \mathbf A が羃化可能 (well powered): 各々の対象  A は部分対象  S \rightarrowtail A の集合を一つしかもたない

最後の「部分対象の集合を一つしかもたない」は何を意味するのかがわかりません。原書が手元になかったので,原文の元になっているらしい PDF(http://www.andrew.cmu.edu/course/80-413-713/notes/ の chap09.pdf)を見てみると,対応する部分は次のようになっています。

1.  \mathbf A is well powered: each object  A has at most a set of subobjects  S \rightarrowtail A

この表現,well powered の定義を知っていればまあわかりますが,意味がとりにくいかもしれません。"at most a set" で「(高々)set size である」を意味しているのだと思います。だから定義全体としては「どの対象についても,その部分対象の全体は集合である(proper class になるほどたくさんは存在しない)」という意味になります。

ちなみに nlab の well-powered category を見ると,定義は

A category C is well-powered if every object has a small poset of subobjects.

となっています。small という語がある分だけ,こっちのほうがわかりやすいかも。

*1:「局所スモール完備圏」はひとまとまりの用語かと思ったら,原文では "locally small, complete category" となっていました。それだったら全部つなげないで「局所スモールかつ完備な圏」とかにすれば紛れがないのにと思いますが,これは好みかもしれません。

既約性

 x^n + x - 1 が既約であることと  n \not \equiv 5 \pmod 6 であることが同値みたいなんだけど,どうやって証明するんだかわからなくて気になってとりあえず調べてみたことを書きます。

http://mathoverflow.net/questions/177789/is-xn-x-1-irreducible によると  x^n - x - 1 は既約なので,それを認めると,n が偶数であれば -x を代入して  x^n + x - 1 も既約であることがわかる。だから奇数の場合の既約性だけが問題になる。

http://math.stackexchange.com/questions/264853/irreducibility-of-xnx1 によると, n \not\equiv 2 \pmod 3 ならば  x^n + x + 1 は既約なので,それをふたたび認めると,n が奇数のとき先程と同様に -x を代入することで  n\not\equiv 2 \pmod 3 ならば  x^n + x - 1 は既約であることがわかる。奇数について  n\not\equiv 2 \pmod 3 n\not\equiv 5 \pmod 6 と同値だから,n が奇数かつ  n\not\equiv 5 \pmod 6 ならば  x^n + x - 1 は既約である。

ということは,これらを合わせると  x\not\equiv5 \pmod 6 ならば  x^n + x - 1 は既約であることがわかる。

 x=5 \pmod 6 のときは  x^n + x - 1 x^2 - x + 1 で割り切れることが容易に確かめられるから,最初に述べた同値性がわかった。

圏論ぐらい普通に生きてればわかる人

世の中には二種類の人間がいる。普通に生きてれば圏論がわかる人と,そうでない人だ。

とかいうのは仮に真だとしても圏論を勉強するうえで何の助けにもならないし,だいたいきれいに二つに分けられるはずもないのですが,しかしある程度は正しいことを言っているのではないかと思います。

圏論に限らず,ものごとの理解の難しさには,人ごとに違いがあります。同じ人でも,対象によって簡単だったり難しかったりします。それが何によって決まっているかといえば,おそらくその人がその瞬間までにどういう経験をしてきたか,でしょう。圏論を理解することについていえば,それがある人にとってどれくらい難しいかは,その人がこれまでにどんな数学的概念にどれだけ親しんできたかに強く依存するでしょう。高校までの数学しか知らない人が圏論を勉強しようとすればかなりの困難が予想されるし,逆に既に抽象代数に慣れている人にとっては圏論の基本的な事項(関手とか極限とか)を理解するくらいは難しくないでしょう。個人的な経験として,普遍写像性を使った議論にははじめから馴染めた記憶がありますが,これはあらかじめ普遍写像性がどういうものかを具体例(直積,商,局所化,テンソル積など)を通じて「既に知っていた」ことが大きく影響しているだろうと思います。いろんな概念が一つの型に納まってしまうのを見て,なるほどうまいことやるものだと感心したものです。

そういう現象は別に数学に限ったことでは全然なくて,例えばスポーツの苦手な人が初めて野球をやったらたぶんバットをボールに当てることができないと思うんですが,できる人は野球をやったことがなくてもきちんと打てたりします。実際,中学のとき同じクラスにスポーツが得意だけど野球はやったことがないらしい人がいましたが,体育の授業でソフトボールをやったらその人は最初からちゃんと打てるんですね。一方,僕は野球はそこそこ好きでたまに友人とやっていたけど,下手なので,あんまり打てない。スポーツのできる彼がいうには「ボールをよく見れば打てる」のだそうですが,よく見ると言われても,できない人にはそもそもそれがどういうことだか想像がつかないのです。

圏論がわかる人とそうでない人の間にもきっと溝があって,わかる人は定義といくつかの例や定理を見て飲み込めるけど,そうでない人はそう簡単にはいかなくて,定義や例や定理をどうやって咀嚼して自分のものにすればいいかわからないのではないでしょうか。「ボールをよく見る」に相当するものが圏論でいうと何なのかはわかりませんが,「定義より明らか」などは近いかもしれません。どちらも簡単なことだと言いたげな言葉遣いですが,それは必要な経験を積んでいる者にしか通じない。

掛け算と割り算は随伴

m が正整数のとき  m x \leq y \iff x \leq \lfloor y/m \rfloor となることを証明する。

適当な仮定の下で  R : \mathcal C \to \mathcal D の左随伴 L は  LD \simeq \lim (\pi : D \downarrow R \to \mathcal C) と表される。そこで  \mathcal C = \mathcal D = \mathbb Z(普通の順序で圏とみなす)かつ  R y = \lfloor y/m \rfloor の場合を考える。すると, \mathbb Z における極限は最小値なので,確かに

 Lx = \lim (\pi : x \downarrow R \to \mathbb Z) = \min \{ y \mid x \le \lfloor y/m \rfloor \} = mx

となることがわかる。