Dr. Sam Sanders Lecture at NII Logic Seminar
Date: February 13, 2013, 13:30--15:30
Place: National Institute of Informatics, Lecture Room 1904 (19th floor) 場所: 国立情報学研究所 19階 1904室 (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/)
Speaker: Dr. Sam Sanders (University of Ghent)
Title: Reuniting the antipodes: Bringing together Nonstandard Analysis and Constructive Analysis
Abstract: Constructive Analysis (aka BISH) was introduced by Errett Bishop as a redevelopment of Mathematics with a focus on computational content. As such, BISH is based on the BHK (Brouwer-Heyting-Kolmogorov) interpretation of logic, where the notions of `proof' and `algorithm' are central. Constructive Reverse Mathematics (CRM) is a spin-off from Harvey Friedman's `Reverse Mathematics' program where the base theory is based on BISH. In this talk, we introduce an interpretation of BISH in classical Nonstandard Analysis. The role of `proof' in this interpretation is played by the Transfer Principle of Nonstandard Analysis. The role of `algorithm' is played by `$\Omega$-invariance'. Intuitively, an object is $\Omega$-invariant if it does not depend on the *choice* of infinitesimal used in its definition. Using this new interpretation, we obtain many of the well-known results form CRM. In particular, all non-constructive principles (like LPO, LLPO, MP, etc) are interpreted as Transfer Principles, which are not available in our nonstandard base theory. Finally, the interpretation preserves the property that not all $\Delta_1$-formulas are decidable in BISH. We discuss applications in (Homotopy) Type Theory.
問合せ先: 龍田 真 (国立情報学研究所) e-mail: [email protected]