Forwarded by Mariko Yasugi [email protected] ----------------------- Original Message ----------------------- From: Yuichi Amitani [email protected] To: Mariko Yasugi [email protected] Cc: CAPE [email protected] Date: Sat, 23 Feb 2013 21:09:37 +0900 Subject: Re: Sam Sandersの講演について伺い ----

-------------------------------- CAPE ワークショップ：An International Workshop on Constructivism 日時：2013年３月１日（金）午後２時〜６時 場所：京都大学総合研究2号館第9講義室 http://www.kyoto-u.ac.jp/en/access/campus/main.htm （34番の建物です）

CAPE International Workshop on Constructivism Date: March 1st (Fri.) 2013, 14:00-18:00 Place: 9th Lecture Room, General Research Building #2 (Sougoukenkyu 2 Goukan ), Kyoto University (No. 34 in the map below: http://www.kyoto-u.ac.jp/en/access/campus/main.htm )

Program (Each slot will have 45 minutes for a talk and 15 minutes for a Q&A session except for general discussion)

2:00-3:00 Yuta Takahashi　(Keio University): On Philosophical Significance of Gentzen's Finitism 3:00-3:10 Break 3:10-4:10 Ryota Akiyoshi (Kyoto University): Brouwer's Proof of the Bar Induction Revisited 4:10-4:20 Break 4:20-5:20 Sam Sanders (The University of Ghent): Nonstandard Analysis: a New Way to Compute 5:20-6:00 General Discussion

Abstracts

Yuta Takahashi　(Keio University): On Philosophical Significance of Gentzen's Finitism

In the 1920s Hilbert proposed the finitary standpoint, on which he aimed to carry out Hilbert's Program. To formulate his finitary standpoint, he attempted to find the fundamental concepts in mathematics. Gentzen's finitism also made this attempt, though he had to extend Hilbert's standpoint due to G"{o}del's incompleteness theorems. Particularly, in the 1935 consistency proof of $PA$ Gentzen included intuitionistic concepts such as the concept of choice sequences among the fundamental concepts. From philosophical point of view, their formulations of the fundamental concepts in mathematics are of remarkable importance.

In this talk, we claim that by admitting choice sequences Gentzen extended the finitist conception of potential infinity. The concept of infinitely proceeding sequences generated by some calculation-rules is a typical infinite concept which can be found in Hilbert's finitary standpoint. However, Gentzen's finitism admits the infinitely proceeding sequences generated by free choices as well as ones generated by some rules. We conclude that in this respect he extended the concept of potential infinity which belongs to the finitist foundations of mathematics and this extension made his conception of potential infinity similar to intuitionists' one.

Ryota Akiyoshi (Kyoto University): Brouwer's Proof of the Bar Induction Revisited

In a series of papers, Brouwer had developed intuitionistic analysis, especially the theory of choice sequence. An important theorem called the ``fan theorem" is used in the development of intuitionistic analysis. The fan theorem was derived from another stronger theorem called the ``bar induction".

Brouwer's argument for a justification of the bar induction contains a controversial assumption on canonical proofs of some formula. Constructive mathematicians have assumed the bar induction as axiom, hence the assumption has not been examined by them. On the other hand, Sundholm and van Atten claimed that the assumption should be regarded as transcendental one in the sense of Kant. They, however, did not give an explanation of why Brouwer needed such a problematic assumption.

In this talk, we sketch a novel analysis of Brouwer's argument via infinitary proof theory. In particular, we point out that there is a close similarity between Brouwer's argument and Buchholz' the method of the $\Omega$-rule. By comparing these two arguments, we give a natural explanation of why Brouwer needed the assumption. If time is permitting, we list some open questions and problems.

Sam Sanders (The University of Ghent) : Nonstandard Analysis: a New Way to Compute

The system ERNA is a version of Nonstandard Analysis based on $I \Delta_0+EXP$. Recently, it was shown that many of the equivalences of $WKL_0$ over $RCA_0$ from Reverse Mathematics can be `pushed down' into ERNA's language, while preserving the equivalences, but at the price of replacing equality `=` by `$\approx$', i.e. equality up to infinitesimals from Nonstandard Analysis.

We overview these results concerning ERNA and provide a possible explanation for the above similarity/robustness. In particular, we introduce `$\Omega$-invariance', a simple and elegant notion from Nonstandard Analysis meant to capture the notion of algorithm and Turing machine. Intuitively, an object is $\Omega$-invariant if it does not depend on the *choice* of infinitesimal used in its definition.

We consider results regarding $\Omega$-invariance in classical and (time-permitting) constructive Reverse Mathematics. --------------------- Original Message Ends --------------------