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

「論理と計算のしくみ」を読んでいたら，シーケント計算の推論規則を ∧右，∨左，⊃左は additive ∧左，∨右 は multiplicative にすると命題論理では contraction が不要になるということを知りました。こういう組み合わせは証明論的にはだいぶ気持ち悪いよう…

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

が既約であることと であることが同値みたいなんだけど，どうやって証明するんだかわからなくて気になってとりあえず調べてみたことを書きます。http://mathoverflow.net/questions/177789/is-xn-x-1-irreducible によると は既約なので，それを認めると，n …

世の中には二種類の人間がいる。普通に生きてれば圏論がわかる人と，そうでない人だ。とかいうのは仮に真だとしても圏論を勉強するうえで何の助けにもならないし，だいたいきれいに二つに分けられるはずもないのですが，しかしある程度は正しいことを言って…

m が正整数のとき となることを証明する。適当な仮定の下で の左随伴 L は と表される。そこで （普通の順序で圏とみなす）かつ の場合を考える。すると， における極限は最小値なので，確かにとなることがわかる。

多項式を微分すると指数が係数に出てくるのって，積の微分の公式 と を使って とかやると出てくる。ということに，多項式を計算機上でいじることについて考えていて初めて気付いた。

ぼくにとって，数学といえば積分らしい。それはきっと昔からそうで，ぼくにとって「積分」という言葉と積分記号は特別なものなのだろうと思う。例えば，あなたが誰かに向かって数学の話をしているところを想像して下さいと言われたら，黒板かホワイトボード…

Lean 本体 最初，github にあるソースを自分でコンパイルしようとしたらうまくいかなかった。apt-get で入るので始めからそうすればよかった。https://leanprover.github.io/download/ に環境ごとのインストールのしかたが書いてある。 Emacs の lean-mode E…

「普通においしい」「普通に嫌い」「普通に言う」などの表現に違和感がある。自己の判断を述べる際に，なぜわざわざ「普通に」と付けるのか。どういう意味で普通だと言っているのかよくわからないし，そもそもそんな疑問が浮かぶ以前に，響きに違和感がある…

well-definedness 周りの議論ってわりと何してるのかわかりにくくない？ と思って考えてたら universality のほうがわかりやすい気がしてきりしたので書いてみた。以下 , は集合， は 上の同値関係。 well-defined とは 写像 が well-defined であるとはどう…

二年前に 直観主義と選択公理の話 という記事を書いたのですが，それに近い内容の論文を 2006 年に Martin-Löf が書いていたこと知りました。"100 Years of Zermelo’s Axiom of Choice: What was the Problem with It?" というタイトルの論文で，Springer か…

何がきっかけか忘れたのですが，一般に n 次元の重箱には隅が 2^(n-1) 個あるのだなということを思ったので，たいした話ではありませんが書いてみることにしました。n 次元重箱とは，n 次元立方体の境界から一つの側面の内部を除いた図形である。具体的には…

ある日の夜，寝ようとして布団に入った瞬間に，どういうわけか 676 という数字が浮かんできた。見覚えのある数字だ。でもどこで見たのだろうか。平方数か何かだろうか。そういえば 24 の二乗はそんな感じの数だった気がする。そこで計算してみると ，ちょっ…

掛け算記号の左右の役割は異なるので順番を入れ換えてはいけないという立場がある。左側は「一単位あたりいくつ」を表し，右側は「何単位分あるか」を表すのであり，それらを逆に書いてはいけないのだという。例えば，2×3=6 と書いたらそれは「三人がそれぞ…

先日 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 i…