ハイティング代数の勉強

J. ヨスト著, 清水勇二訳 現代数学の基本概念 上 を読んでいて、p.35 の練習問題が難しかったので、この問題について書いておく。

p.35の練習問題とは、ハイティング代数において以下を示すことだ。

t \Rightarrow (s \Rightarrow u) = t \land s \Rightarrow u

ハイティング代数は0と1を持つ束で冪対象 u^{s} = s \Rightarrow uを持つ。

冪対象の記法で書くと示したいことは以下になる。

(u^{s})^{t} = u^{t \land s}

xを任意の元として、次の①と②, ②と③は一対一に対応する。ここで \toは \leを表す。

① x \land t \land s \to u

② x \land t \to u^{s}

③ x \to (u^{s})^{t}

また、 yを任意の元として、次の④と⑤は一対一対応する。

④ y \land t \land s \to u

⑤ y \to u^{t \land s}

もし①で xを u^{t \land s}とした射があるならば、③の xに u^{t \land s}を代入して、射

u^{t \land s} \to (u^{s})^{t}

が存在する。すなわち以下が成り立つ。

u^{t \land s} \le (u^{s})^{t}

一方、もし④で yを (u^{s})^{t}とした射があるならば、⑤の yに (u^{s})^{t}を代入して、射

(u^{s})^{t} \to u^{t \land s}

が存在する。すなわち以下が成り立つ。

(u^{s})^{t} \le u^{t \land s}

したがって、 u^{t \land s} \le (u^{s})^{t}, (u^{s})^{t} \le u^{t \land s}, 反対称律より

(u^{s})^{t} = u^{t \land s}

となる。

あとは、 u^{t \land s} \land t \land s \le uと (u^{s})^{t} \land t \land s \le uを示せばよい。

まず、 u^{t \land s} \land t \land s \le uは、 u^{t \land s} \le u^{t \land s}から成り立つことがわかる。

次に、 (u^{s})^{t} \land t \land s \le uは、次のように示す。

(u^{s})^{t} \le (u^{s})^{t} \Leftrightarrow (u^{s})^{t} \land t \le u^{s} \Leftrightarrow (u^{s})^{t} \land t \land s \le u