↓これの続き cut-elimination.hatenablog.com を順序集合とする。 の要素 を任意にとったとき、集合 の上限 と下限 が存在する場合、 は束(そく)であるという。 を 、 を と書くことが多い。 と を持つことを明示するために束 を と書くこともある。 前に出…

↓これの続き cut-elimination.hatenablog.com を順序集合とする。部分集合 をとる。 がすべての について のとき、 は の上界であるという。例えば順序集合 について の部分集合 をとると、 なんかはその上界である。 順序集合 と について、 を の上界をす…

当ブログは論理学とアニメを両輪とするはずが、気付けばアニメばかりになっている！ アイデンティティの危機である。何故アニメばかりになったのかというと書きやすいからである。論理学記事は数式を打つのが面倒臭い。また私の専門(?)分野である証明論は証…

とある論文を読んでいて余帰納法の知識が必要になったので調べた。その論文ではJacobs & Rutten "A tutorial on (co)algebras and (co)induction"で入門するとよいとあったのだが、同論文のような圏と関手を使った議論はそんなに必要そうではなかった。 で、…

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

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

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

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

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

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