應用邏輯討論會系列 (XIX) -- A simplification of the Kreisel-Goodman Theory of Constructions
- 講者Hidenori Kurokawa 教授 (神戶大學資訊科學系)
邀請人：廖純中 - 時間2015-03-13 (Fri.) 15:00 ~ 17:00
- 地點資訊所新館106演講廳
摘要
In this talk, we discuss Kreisel-Goodman's Theory of Constructions (ToC). This theory was originally introduced by Kreisel as an untyped theory which can handle the notion of mathematical constructions used in the BHK interpretation of intuitionistic logical constants. One of the theoretical goals of ToC is to provide a formal theory of mathematical constructions [@BackSlash]in terms of which the formal rules of Heyting's predicate calculus [HPC] can be interpreted (Kreisel, 1962)." However, the version of ToC which satis_es all the desiderata considered by Kreisel turns out to be inconsistent (the Kreisel-Goodman paradox).
We _first present our own analysis of the paradox and propose a consistent sub-theory of the inconsistent version of ToC. We then discuss an outline of Goodman's proof of the soundness of the interpretation of HPC into this weaker version of ToC. This is a joint work with Walter Dean.