※この記事はエイプリルフールのビッグウェーブに乗り遅れないように焦って書いたので、内容が凄くテキトーです。のちのちちゃんと勉強して推敲してアップデートします。 「私は嘘つきです」というやつです。論理学っぽく書くと「この文は偽である」。 (1)「…

ロジックを勉強していたら誰もが(?)出くわす束縛変数の名前の付け替えのやつをまとめたいのよ。 以下のことを書いていて気づいたのだが、"Basic Proof Theory*1"（以下：BPT）には式 expressions や論理式 formulas の定義がない。subformulas の定義はある…

Troelstra先生とSchwichtenberg先生*1の"Basic Proof Theory"もまあ必読書なのでしょうな。頑張ります。 単純型付ラムダ計算の代入補題についてメモ。 代入は以下のように項の複雑性によって帰納的に定義される。 , （ でないとき*2）, , , （ でないとき。w…

Awodey先生は「アウディ」と読むらしい。数学者・数理論理学者であり数学の哲学者*1でもある。こういう人はすごいと思う。「数学の基礎付け」なんてのはいまや死語かもしれないけれど、圏論は型理論との相性が良くて、計算機科学を考慮した新機軸がいろいろ…

これまで完全性定理やカット除去定理についてごちゃごちゃ書いてきて気づいたことがある。他の分野の数学の定理ではあまりないのかもしれないが、ロジックのメタ定理というのは、独特の語りにくさ？ みたいなのがある。完全性定理だとかカット除去定理だとか…

完全性定理も中途半端なところで停滞しているのに、新シリーズとしてカット除去定理を考える。カット除去定理もロジックの教科書ではよく登場していて*1、その証明は完全性定理以上に教科書ごとに個性が出ている。そういうのを比較考察していきたいのだけれ…