「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ六「等号の規則」「仮定付判断と代入規則」（復習編）

　お休みを挟んでこれの復習編。

等号の規則

　これは導出可能規則と言ってもよさそうだけど、どうも導出体系ではないという点が重要そうなのでそうは言えない。特にカノニカルな要素を得る計算というのはあまりフォーマルに導入されていない。

　 $A$ が集合だと言っても、 $A$ という全体がプラトニックにあると考えてはいけない。 $A$ の全体は $A$ のカノニカルな要素の形成の規定によって与えられるものである。これは次節「集合とカテゴリー」で詳述される。この点、ひとつひとつの判断（judgement）を基礎としているのは直観主義の新(?)機軸という感じで哲学的にも興味深い。なんかポエティックになってしまった。

仮定付判断と代入規則

　予習編で「 $B(x) \; set \; (x \in A)$ という判断は現在の標準的な記法では $x:A \vdash B(x) \; set \; (type)$ となるはず」と書いたが、しかし $x \in A$ はなんらかの規則が適用されて discharge されたときカッコに入れるとあり、なんだか記法に自信が持てなくなってきた。discharge されてしまったら仮定付判断とは言えないような気がする。これは実際に discharge する規則が出てくるまで保留ということになった。

　問題の "like the one that we are in the process of building up" は匂わせということで落ち着いた。

　 $b(x) \in B(x)$ のようなのの $x$ は背後に全称量化があるような感じがするという話が出た。しかしこれはラムダ計算でやるような関数が念頭にあると思う。ロジック脳だと全称量化（や存在量化）を使って関数を定義するが、ITTでは関数をプリミティブとして全称量化に相当するものを定義する、という発想がよいのではないかということになった。