「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ壱「緒言」「命題と判断」（予習編） - 曇りなき眼で見定めブログPer Martin-Löfの"Intuitionistic Type Theory"(1984)、通称ITT84*1の勉強会の記録でござる。今回はとりあえず、最初の2節で読んでもわからなかったところをメモっときます。 個人的な動機 緒言（Introductory remarks） ロジックと数学の関係 ラッセルの型理論 『プリンキピア』 可述性がわからん さらにITT84でわからんところ プログラミング言語との親和性 命題と判断（Proposition and judgements） 命題と判断の違い 判断とは？ BHK解釈 岡本賢吾先生の論文を読もう そういえば証明ってなんなのだろうか 個人的な動機 なにゆえITTに興味を持ったのかを書いといたほうがのちのち振り返ったときによいかもしれない。 私は論理と計算の対応という現象に興味がある。なかでもITTは、めちゃくちゃ基礎的な理論でありな
