曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾九「二つの集合の直和」「命題的な(?)等しさ」(予習編)

 過去のシリーズはこちらから。

 今回は自分の担当ではないので内容がないよう。

二つの集合の直和

 数を指定しない直和は連言になって二つの集合の直和は選言になるというのはなんか凄い。

 {\textsf D} というまた新しいのが出てきた。

命題的な(?)等しさ

 "propositional"はここではどう訳すべきか。「命題の」等しさではないので、「命題としての」等しさとかか。

 この I の導入則はなんかせこいような!? ちょっとメタなが話が体系内に入っている感じがする。しかし非常に面白い。