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

となることがわかる。

多項式の微分は積の微分から出てくる

多項式を微分すると指数が係数に出てくるのって，積の微分の公式 (fg)' = f' \cdot g + f\cdot g' と x' = 1 を使って

(x^2)' = x' \cdot x + x \cdot x' = x + x = 2x
(x^3)' = (x^2)' \cdot x + x^2 \cdot x' = 2x^2 + x^2 = 3x^2

とかやると出てくる。

ということに，多項式を計算機上でいじることについて考えていて初めて気付いた。

積分

日常

ぼくにとって，数学といえば積分らしい。

それはきっと昔からそうで，ぼくにとって「積分」という言葉と積分記号は特別なものなのだろうと思う。例えば，あなたが誰かに向かって数学の話をしているところを想像して下さいと言われたら，黒板かホワイトボードに積分記号を書いているところを思い浮かべそうな気がする。普段は解析を使うようなことをあまりしないから，積分という概念自体はそれほど身近なものとはいえなくなっている気がするけど，そうなってから何年も経ってもやはりぼくにとって積分の特別さは変わらないものらしい。

どうして積分なのか，ということは，長い間気にしたことがないどころか，積分というものが頭の中の目立つ場所に居座っていることに気付いてすらいなかった。数年前にようやく，どういうきっかけだったか忘れたが，どうやらぼくの頭には積分という言葉が頻繁に浮かんできているようだということに気がついた。その後もそれがなぜなのかを考えた記憶はほとんどない。ところがこの間突然，これもきっかけは忘れてしまったが，もしかしたらあれではないかという記憶に思い当たった。中学の数学の授業中に積分の話を少しだけ聞いたことがあって，それが高校生になって実際に積分を学ぶまでずっと気になっていたのだ。

その中学の授業中に聞いた話というのは，扇形の面積が「半径×弧長÷2」になるということを習ったときに余談として出てきたものだ。この面積の式は三角形のそれと似ているけど，これは偶然ではなくて，細い三角形が無数に並んでいるとみなして計算すればこうなると理解できるということ。それから，今のは厳密ではない説明だけど，積分というのがあって，それを使うとこのアイデアはもっと厳密な議論に落とし込むことができるのだということ。その二つのことを聞いたのだと思う。

それ以上の説明は聞かなかったから，積分というものがどういうものなのかはわからなかった。でも，その時に出てきた「積分」という言葉はそれ以来ずっと覚えていたし，何か気になる，という気持ちを持ち続けていた。過去を思い返してみると，数学に対する興味は昔からあっても，具体的な数学の概念に対して興味を持ったことはそれまでにはなかった気がする。だからもしかすると「よくわからないけどおもしろそうだ」とかいうことを思ったのはそれが最初だったのかもしれない。そういうことがあったから，ぼくの頭の中では「積分」という言葉やあの記号が何か数学の魅力の象徴のようなものとして位置付けられているのだろうか。