上限を適当に決めて，サイズがそれ以下の lambda term の個数はいくつになるか計算してみました。本当に項の個数を数えると変数の名前を変えるだけでいくらでもできるので，自由変数として使える変数の個数を制限します。この条件は都合のいいように設定した…

最近，古典論理に対応する計算体系について勉強してます。古典論理だと Peirce's law と call/cc が対応するとかいう話がわりと有名で，基本的にはコントロールオペレータを含む体系になります。それで，そこにさらに様相が入った場合にはどんなことになるの…