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

TOP

TOP

TOP

TOP