Applied Logics Seminar Series (XIX) -- A simplification of the Kreisel-Goodman Theory of Constructions
- LecturerProf. Hidenori Kurokawa (Kobe University)
Host: Churn-Jung Liau - Time2015-03-13 (Fri.) 15:00 ~ 17:00
- LocationAuditorium 106 at new IIS Building
Abstract
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.