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

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

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾六「直和の応用(途中から)」(復習編)

 こちらの復習編。

左射影

 p(c) の依存型のときの論理読み(存在量化のとき)というのは、B(x) の witness を取り出すということになろうかと。それがヒルベルトのアレになる。右射影だとその個体について成り立つ性質を取り出すことになる。

右射影

 左射影と同じように、\Sigma規則のインスタンスであることをわかりやすくしました。

f:id:cut_elimination:20210618183219j:plain

形成則について

 \supset や & の形成則にある、A \; true を仮定して B \; prop. が出てくるというのは、具体的にどういう状況だろう???

\Pi導入則とラムダ抽象

 \Pi導入則の依存なしバージョンがラムダ抽象ということでよいのだろうか。

&について

 論理学の入門とかでやる自然演繹では A&BAB は平等だが、ITTでは非対称的である。これがおもしろい。