λλλ

λ式をガリガリと解いている。
論理学の教科書だと束縛変数と自由変数の定義が日本語で書かれていて付帯条件が満足かどうか判断するのが微妙に手間だったりするのだが、今回の授業の資料では関数・集合論的に書かれていて、あぁこういうアルゴリズム的に判断できるのだなと理解した。遅いっつぅの俺。
後、某所の自然数論は矛盾しているって証明にはびびった。