「古典論理は可換環論なんだよ」のなかに、
- 愚直にrudimentary calculationを実行してください。
- これまたひたすら単純計算をすれば、…
- これも、紙と鉛筆と手で単純計算あるのみ。
という表現がありますが、僕は実際には計算してなかったので、やってみました（疲れた）。計算で確認すべきことは：
- MICR（乗法的ベキ等可換環）からBL（ブール束）がちゃんと作れること
- BLからMICRがちゃんと作れること
- MICR→BL→MICRでもとに戻ること
- BL→MICR→BLでもとに戻ること
途中で失敗したりしているけど：
- 計算用紙 1：MICR→BLの確認、うまくいった。[追記]BL側の∧ベキ等律を忘れているけど、x∧x := x + x + xx = x + x + x = x 。[/追記]
- 計算用紙 2：BL→MICRの確認、分配律のところで挫折。
- 計算用紙 3：BL→MICRの分配律、なんとかなった。
- 計算用紙 4：MICR→BL→MICRとBL→MICR→BLの確認、実際には一回失敗していて、もう一枚の計算用紙で“練習”している。
ブール束から定義した可換環（となるはずの代数系）における分配律と、BL→MICR→BLでミート（∧）が再現することを確認するときにワケワカラナクなっています。で、“オリジナルの状況”に戻ってうまくいことを再確認して、オリジナル計算を真似てもう一度やり直し。
この“オリジナルの状況”とは：
- 普通の集合ブール束（ベキ集合）は、対称差 X△Y := (X＼Y)∪(Y＼X) = (X∩Yc)∪(Y∩Xc) を加法、∩を乗法とすれば、乗法的ベキ等可換環となる
というものです。この事実は見やすく確認も容易です。これをもとに、双対原理により“ひっくり返した”定義が「古典論理は可換環論なんだよ」で紹介した定義です。人為的にひっくり返しているため、直観が働きにくくなってしまうんですよね。
実は、Tを1に対応させることも出来て、そのほうが関手の構成は直観的で楽だったりします。
とはそういう事情を言っています。
後で見て混乱しないように注意：
- 記法は計算ごとに少しずつ変えています。
- 束演算から定義された加法を#、乗法を・とか*で表しているところがあります。
- 主に束演算を行うところでは、x∨y→x + y, x∧y→xy, ¬x→x'と書いています。この記法だと、加法が乗法に対して分配するところが奇妙になるので注意。
- 環演算から定義された∧をΠで表しているところがあります。
[追記 date="翌日"]「trueを0にしたほうが計算がスムーズ」なんて言ったことが発端で話をはじめたのだけど、別に計算はスムーズじゃないね。「人為的にひっくり返しているため、直観が働きにくくなってしまうんですよね」、というわけで、めんどくさい（天下りに双対原理を使って計算を避けることもできるが）。実際は、「trueを0にしたほうが可換環論との対応がスムーズ」ってことでした。[/追記]
