- English HOME
- Center for Applied Philosophy and Ethics
- CAPE International Workshop on Constructivism

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 of the map in

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 Akiyosh (Kyoto University):
Brouwer’s Proof of the Bar Induction Revisitedi**

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.

** **

TOP