最初の案： 暫定版 証明図シリアル化構文 - 檜山正幸のキマイラ飼育記 メモ編 その後の変更： 証明図シリアル化構文 キーワードの現状 - 檜山正幸のキマイラ飼育記 メモ編 BLKと書いてあるのはブロック、そうでなければコマンド。 論理記号 導入 削除 ∧ make…

演繹付きインスティチューション〈institution with deduction〉を定義する。普通のインスティチューションに、指標Σごとの演繹性判断〈deducibility judgement〉|-Σが付いている。 |-Σは、Pow(Sen[Σ])とSen[Σ]のあいだの（二項）関係 演繹性判断は、次の公…