ゲーデルの System T について

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