[kisoron-ml] Dr. Sam Sanders Lecture at NII Logic Seminar

[Makoto Tatsuta]

	     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: tatsuta at nii.ac.jp