本日始めて知ったこと。ゲーデルの本来の枠組みは（単純型理論を含む公理系であって）induction scheme も含む事。 "Proofs and Types"では単純型理論として紹介され、induction axiom は含んでいません。恥ずかしながら、これしか読んだ事ありませんでした。…

晴れ、湿度は依然として高い。ついでに、咳がまだ止まらない。 起床は9時半、出勤して会議と打ち合わせ。それから発表準備をする。帰宅は21時15分、夕食は肉じゃが。