ロジックを勉強していたら誰もが(?)出くわす束縛変数の名前の付け替えのやつをまとめたいのよ。 以下のことを書いていて気づいたのだが、"Basic Proof Theory*1"（以下：BPT）には式 expressions や論理式 formulas の定義がない。subformulas の定義はあるので論理式の定義は暗になされているのだろうが、式はどうだろう。論理式を式に含めてよいのかどうか今のところハッキリとはわからない。もうちょっとちゃんと読み進めないと。しかしどうも含めていそうなので、以下では式の例として論理式を使っています。論理式や項 term の総称が式じゃないかなと。 BPSの3…
