ABM 2015, Arbeitstagung Bern-München
17.12.2015-18.12.2015
Place
Mathematics Institute LMU, Room B 349.
Welcome dinner
Alter Simpl18:30, Türkenstrasse 57
Thursday Talks
09:30-10:30, Stanley Wainer: "Some generalized Goodstein sequences" (j.w.w. T. Arai and A. Weiermann)
10:30-11:00, Coffee Break
11:00-11:45, Dieter Probst: "Well-ordering meta-predicative theories using methods from impredicative proof theory"
11:45-12:30, Kentaro Sato: "Flumini-Sato's theorem and ordinals for ACAo' type systems"
12:30-15:00, Lunch break
15:00-15:45, Chuangjie Xu: "A constructive manifestation of the Kleene-Kreisel continuous functionals"
15:45-16:30, Daniel Wessel: "On Zorn, Frobenius, and Excluded Middle" (j.w.w. Peter Schuster)
16:30-17:00, Michel Marti: "Intuitionistic Distributed Knowledge "
Thursday dinner
Los Faroles18:00, Nordendstrasse 26
Friday Talks
- 09:30-10:15, Sam Sanders: "The Gandy-Hyland functional in Nonstandard Analysis"
- 10:15-11:00, Josef Berger: "Convexity and constructive infima"
Abstracts
- Stanley Wainer: "Some generalized Goodstein sequences" (j.w.w. T. Arai and A. Weiermann)
There is a strong analogy between Veblen's function enumerating
normal functions on ordinals, and a parameterized version of the Ackermann function (in fact they are defined by essentially the same recursion).
This analogy is exploited here, to produce a variety of Goodstein-style independence results, e.g. for ATR0
and ID1.
- Kentaro Sato: "Flumini-Sato's theorem and ordinals for ACAo' type systems"
Flumini-Sato's theorem asserts that the iterated Π01 comprehension with parameters along a binary relation
implies the well-foundedness of the relation. While this was published only last year, it has then turned out (to the speaker)
that a similar result for parameter-free Π11 had appeared in Arai's paper in 80s as a result of Takeuti.
Although this becomes quite delicate for parameter-free Π01, we apply it to obtain the proof theoretic ordinal
of ACA′0 type systems, namely those whose characteristic axioms are the existence of ξ-th relativized
jump for any ξ below α where 'for any' is taken internally.
- Chuangjie Xu: "A constructive manifestation of the Kleene-Kreisel continuous functionals"
In the category of Kleene-Kreisel continuous functionals, all maps from the Cantor space to the natural numbers are uniformly continuous.
However, its traditional treatment available in the literature relies on either classical logic or constructively contentious principles.
In a weak constructive setting, we develop the theory of Kleene-Kreisel spaces within a category of concrete sheaves, called C-spaces,
which form a locally cartesian closed category. This category has a fan functional and validates the uniform-continuity axiom in System T
and dependent types. We do not need to assume Brouwerian continuity axioms,
but, if we do, then we can show constructively that the full type hierarchy is equivalent to our manifestation of the continuous functionals.
- Daniel Wessel: "On Zorn, Frobenius, and Excluded Middle" (j.w.w. Peter Schuster)
As opposed to the Axiom of Choice proper, Zorn's Lemma allegedly lacks non-constructive consequences. While our recent attempt to
relativise this assertion has not yet led to the desired result, it has already prompted some not uninteresting order-theoretic equivalents of
the Law of Excluded Middle. A key role is played by the Dual Frobenius Law.
- Sam Sanders: "The Gandy-Hyland functional in Nonstandard Analysis"
We show that the (non-computable) Gandy-Hyland functional can be approximated
by a primitive recursive term (from Goedel?s T) involving nonstandard numbers inside
Nelson?s internal set theory. From this classical and highly non-effective proof, we
extract a term which computes the Gandy-Hyland functional in terms of the fan functional
and a modulus-of-continuity-functional.
Accommodation
Organizers
Last change
08. December 2015
