19/03/21 18:11:01.10 L2G86nzK.net
>>638
つづき
定数、関数、述語の意味：
?0? = (自然数の0) ?0?∈N
?1? = (自然数の1) ?1?∈N
?a? = (自然数の足し算 +N) ?a?∈Map(N×N, N)
?e? = (自然数の等号 =N) ?e?∈Rel(N, N)、Relは二項関係の集合
このような定義の後で、項'a(1,1)'とか論理式'e(a(0,1), a(1,0))'などの意味が計算できます。
?a(1,1)?
= ?a?(?1?,?1?)
= +N(1,1)
= 自然数としての 1 + 1
= 2
?e(a(0,1), a(1,0))?
= =N(+N(0,1), +N(1,0))
= =N(1, 1)
= 自然数に関する命題 “1 = 1”
= true
どうでしょうか？ しっちめんどくさいなー！ と思いませんか。面倒でもこういうキッチリした議論を一度くらいは体験する価値はあるかも知れません。けど、一度で十分。僕は毎度繰り返す気力はありません。したがって、このテの話は割愛します。
次のような方針にします。
おわりに
僕がこの記事を書いた動機は、ローヴェル流の限量随伴性（quantification adjunction）に付随するニョロニョロ関係式が、自然演繹風証明図の同値変形に対応することを紹介したかったからです。その割には、随伴などの圏論的概念と証明図との関係をあまり述べていません。この辺を述べると、現状の証明図の欠陥を指摘することになり、まーた自然演繹の悪口になります。
(引用終り)
以上