Per Martin-Löfの"Intuitionistic Type Theory"(1984)、通称ITT84*1の勉強会の記録でござる。今回はとりあえず、最初の2節で読んでもわからなかったところをメモっときます。 個人的な動機 緒言(Introductory remarks) ロジックと数学の関係 ラッセルの型理論 『プリンキピア』 可述性がわからん さらにITT84でわからんところ プログラミング言語との親和性 命題と判断(Proposition and judgements) 命題と判断の違い 判断とは? BHK解釈 岡本賢吾先生の論文を読もう そういえば証明ってなんなのだろうか 個…