Troelstra先生の"Lectures on Linear Logic"を読んで線形論理の代数的意味論を勉強している。
いま本では大幅に省かれている様相なしの古典述語線形論理の健全性定理の証明ができたっぽいところ。
Troelstra先生はジラール先生のオリジナルとは違った記法を使うのだが、代数的意味論をやるとその一部は何故その記法なのか分ってくる。& と が
と
で代替されるのだが、これは代数的には束の下限と上限になるからである。これに慣れてしまうと & と
に違和感がある。
は
で代替されている。これは何故か分らない。圏論的にはモノイド積になるのでこれでいい感じがする。
モノイド積ってデカルト積と何が違うのかなあと思っていたが、一般に から
や
は出てこないので射影が出来ないことになるなあ、など。
