Troelstra進捗

今日はTroelstraの最初の最初を努力して読んだ. Classical Linear Logic (CLL)とIntuitionistic Linear Logic (ILL)の導入と諸Propositionを追った. とりあえずantecedentsのsequentは直感的にはテンソルで繋がれていて, succedentsのsequentは直感的には℘で繋がれているという認識でよいということがわかった. それにしても

以下は証明可能. 証明はすぐにできる.

と書かれた後に20個ぐらい下に式が連なっていてあまりにも埋めるのが面倒くさかった.