Awodey『圏論』第6章その3 (6.6から）

圏論

直観主義命題計算と型付きラムダ計算がCurry-Howard対応で同型になるということは計算機の世界ではよく知られているらしいが、命題6.14では直観主義命題計算にはハイティング代数、命題6.17ではラムダ計算にはデカルト閉圏に対して完全性定理が述べられており、いまひとつ同型性が見えてはこないのだが...まあ、ハイティング代数はデカルト閉圏だからいいのか...と思っていたら、正部分という制限はあるものの6.7節でクリプキモデルによる統一があって、落ちがついた. ただ、クリプキモデルというと様相論理のモデルだと思っていたので、こんなところで出てくるのは意外であった. なかなか深いが、ここはさらっと流す章という気がする(p.160の宿題を全部は解いていない言いわけです)．ただ、命題6.19はちょっと面白い．


p.156の宿題．
・ \tilde{(\epsilon\circ (g\times 1_A))}=g
<証明>
\epsilon\circ (g\times 1_A)
[tex: =\lambda x.(\lambda z.fst(z)snd(z)(\lambda w.))x]
[tex: =\lambda x.(\lambda z.fst(z)snd(z))]
=\lambda x.g(fst(x))snd(x)
∴ \tilde{(\epsilon\circ (g\times 1_A))}
[tex: =\lambda z \lambda x.(\lambda y.g(fst(y))snd(y))]
=\lambda z \lambda x.g(z)x
=g


p.160の宿題をひとつだけ解く．
・2^Iはハイティング代数である．<証明>
半順序集合の構造はpointwiseに入れる．
0はIの元をすべて \botに対応させる写像、1はすべて\topに対応させる写像とする．
(p\wedge q)(i)\equiv min(p(i),q(i)).
(p\vee q)(i)\equiv max(p(i),q(i)).
ここにmin(x,y)はx,yのいずれかが\botのとき\bot、それ以外のとき\topを返す関数、max(x,y)はx,yのいずれかが\topのとき\top、それ以外のとき\botを返す関数である．
問題は冪であるが、次のように定義する.
(p\Rightarrow q)(i)\equiv imply(p(i),q(i)).
ここにimply(x,y)はxが\topかつyが\botのとき\bot、それ以外のとき\topを返す関数である. 要するに"ならば"の論理演算である。p.146の定義6.8の3の成立を示す.
(a\wedge b \le c iff a \le (b \Rightarrow c))
min(a(i),b(i)) \le c(i)が成立することとa(i)\le imply(b(i),c(i))が成立することが同値であることを見る．まずc(i)が\topの場合は自動的にimply(b(i),c(i))=\topなのでどちらも成立している. c(i)が\botとすると、左辺が成立するのは、a(i)、b(i)のどちらかが\botという場合のみである．imply(x,y)の定義から右辺の成立条件もこれに同じであることがわかる．□


　　******

p.155 4行目（てつさん指摘分）
　誤『境界変数名』
　正『束縛変数名』


p.155 7行目（てつさん指摘分）
　誤『恒等式』
　正『恒等射』


p.157 下から5行目
　誤『演繹的に健全』
　正『健全』？
　原文『deductively sound』

　調べた範囲では、"演繹的に健全"あるいは"演繹的健全"という用語は無いように思われます. 通常は"deductively sound"と"健全"は同じ定義で、わざわざ"演繹的"というと"演繹的でない健全性"というものあるような誤解を生むかも...生まないかも...


p.158 下から12行目（てつさん指摘分）
　誤『識別する』
　正『同一視する』
　原文『identifying』


p.160 1行目（てつさん指摘分）
　誤『同等に定式化される』
　正『同値的に定式化される』
　原文『equivalently formulated』
　試訳はいまいちです。ここでは2^Iは半順序集合の圏における冪と考えており、一般的な真理値との対応と異なっていますが、それは以下に記述があるように p.159の条件(1)を反映したものです．


p.160 真ん中あたり（てつさん指摘分）
　誤『ハイティング代数において価値のある完全性定理』
　正『ハイティング代数に値を取る完全性定理』
　原文『Heyting-valued completeness theorem』
　はっきりと誤訳です．


p.161 10行目
　誤『理想的な命題2』
　正『理想的な命題真理値2』
　原文『idealized propositions 2』
　んー "命題2"では意味がわからんですが、試訳もいけてないです．どうしましょ．


p.163 下から4行目
　誤『磨けばよい』
　正『精密化すればよい』
　原文『sharpen』
　"磨く"に違和感を感じただけで、ここは趣味の問題です．


p.164 5行目
　誤『以下に与えられることができたならば』
　正『以下に与えられるように』
　原文『to be given below』
　はっきりと誤訳です．