Abstracts

Arnold Beckmann — "Provably Total NP Search Problems of Bounded Arithmetic and beyond"

Bounded Arithmetic forms a collection of weak theories of Arithmetic related to complexity classes of functions like the Polynomial Time Hierarchy. Many connections between Bounded Arithmetic and important questions about complexity classes have already been established. Recent research considers total NP search problems in the context of Bounded Arithmetic. Total NP search problems have been studied by Papadimitriou et al as a means to characterise the complexity of natural search problems which cannot be analysed as decision problems.

In my talk I will review the research programme of characterising the provably total NP search problems in Bounded Arithmetic, and explain why it is important for current research questions in the area. I will describe recent results about the provably total NP search problems of a Bounded Arithmetic theories related to PSPACE and EXPTIME reasoning. I will also describe this program for theories beyond Bounded Arithmetic like Peano arithmetic, and what impact this might have on Complexity Theory.

Benno van den Berg — "Arithmetical conservation results and Goodman’s Theorem"

A well-known result by Goodman [1] states that Heyting arithmetic in all finites types together with the axiom of choice for all types is conservative over Heyting arithmetic. Goodman’s original proof was quite complicated and many people have since tried to give more perspicuous proofs of his theorem, including Goodman himself, Beeson, Renardel de Lavalette, Coquand and possibly others. In this talk I will present my preferred proof, developed together with Lotte van Slooten, which combines ideas from all these authors and adds some new ones.

  [1] N.J. Goodman, The theory of G odel functionals, Journal of Symbolic Logic 41 (3), 1976, pp. 574{582}

Wilfried Buchholz — "Ordinal notations around the Bachmann-Howard ordinal I, II & III"

Various ordinal functions which in the past have been used to describe ordinals not much larger than the Bachmann-Howard ordinal are set into relation. Special efforts are made to reveal the intrinsic connections between Feferman’s θ-functions and the Bachmann hierarchy.

François Dorais — "Provident Sets and Predicative Sets"

We will discuss a new predicative subsystem of set theory due to A. R. D. Mathias [1], which is called PROVI. The key feature of PROVI is the restriction of transfinite recursion to rudimentary functions in the sense of Jensen. With such restrictions, we obtain a stratified understanding of the predicative set theory, while maintaining a fully workable theory of sets at each level. We will show that the lowest level of this hierarchy corresponds to the subsystem of second-order arithmetic ACA+0and explore some higher levels and their correspondence with predicative subsystems of second-order arithmetic.

  [1] A. R. D. Mathias and N. J. Bowler, "Rudimentary Recursion, Gentle Functions and Provident Sets," Notre Dame J. Formal Logic, Volume 56, Number 1 (2015), 3-60.

Kentaro Fujimoto — "Grounded Classical Truth"

A theory of truth takes truth as a primitive predicate operating on sentences. A theory of truth over arithmetic is obtained by adding such a primitive predicate and axioms for it on top of an arithmetical theory. When the scope of the truth predicate includes sentences containing the truth predicate itself, then it is called self-applicable. Due to well-known Liar-type paradoxes, the naive axiomatization of self-applicable truth is inconsistent, and a variety of restrictions of the naive axiomatization have been presented, which result in a number of theories of truth. In this talk, I will present a new theory of truth (over arithmetic) which behave more nicely than many of previously presented theories. If time permits, I'll try to make some comparison to Frege structures and/or unfolding systems. This is a joint work with Volker Halbach.

Iosif Petrakis — "On the geometric character of Homotopy Type Theory"

We explain how the homotopic interpretation of Martin-Löf’s Intentional Type Theory (ITT), given by Voevodsky, Awodey and Warren, provides not only a geometric presentation of the basic concepts of ITT, but also a naturality in its development. We present examples of a ”Thesis of Naturality”, which guides the formation of many theorems of Homotopy Type Theory (HoTT). Moreover, we discuss the synthetic character of HoTT and some questions related to the theory of higher inductive types.

Timotej Rosebrock — "Recursion theory in applicative theories"

The basic theory of operations and numbers BON was introduced by Feferman and Jäger as restricted classical version of the elementary theory of operations and numbers EON by Beeson and the theory APP by Troelstra and van Dalen. These theories give an abstract axiomatization of the partial recursive functions, introduced by Kleene to formalize the concept of a computation. Every object can be looked at as a partial function with arbitrary arity or as an argument; so the application of an object to another object is not necessarily defined. We add induction and a new truncation operator to BON for being able to formalize important aspects of partial recursive functions that are not covered by the theories mentioned above. These additions are natural, since they are valid in several established models. We will have a look at one of them: the graph model, developed by Engeler, Plotkin, and Scott.

Kentaro Sato — "Similarities and Dissimilarities between Second Order Number and Set Theories"

First I overview our recent works on similarities and dissimilarities among second order frameworks, including second order number theory and second order set theory as well as higher order number theory (where only the highest order is seen as the second order and the rests are the first). It has turned out that second order number theory is quite special and the others share several features.

In the second half of the talk, I explain my most recent work in this area, namely several results on the inductive dichotomy scheme, a new weak variant of inductive definition, and its application to the studies of determinacy axioms. We will see that, except in second order number theory, open determinacy is strictly stronger than clopen determinacy. This is another significant difference from second order number theory, where open and clopen determinacies have been known to be equivalent since the origin of reverse mathematics. If time permits, I show that Hausdorff-Kuratowski hierarchy of differences of opens can be faithfully reflected by the hierarchy of consistency strengths of the associated parameter-free determinacy axioms.

Kentaro Sato — "A Partial Realization of Hilbert's Program for Brouwer's Intuitionistic Mathematics"

We identify the fragment of Brouwer's Intuitionistic Mathematics which Hilbert would recognize safe according to his finitism, and then what kind of axioms can be augmented without affecting the consistency strength. Although the original Hilbert's Program was initially developed by the cut-elimination method, our main tool will be double negation, realizability and forcing interpretations.

While this work has already been presented in several occasions by me or by the collaborator since some years ago, in this talk I focus on the analogue of the argument concerning Weak König's Lemma in Hilbert's Program for Classical Mathematics. This lemma should be rejected from Finitistic perspecitve, but the fact that it can be added without affecting consistency strength to the Finitistic Mathematics is a monumental result in Hilbert's Program and plays a central role in Simpson's claim on "partial realizations of Hilbert's Program" for Classical Mathematics. The analogue in Brouwer's Intuitionistic Mathematics is LLPO, Lesser Limited Principle of Omniscience. By the so-called Brouwer's weak counter example argument, we can see that LLPO is rejected from Brouwer's perspective, but I will show that this can be added to the finitistic fragment of Intuitionistic Mathematics without affecting the consistency strength

This is a joint work with Takako Nemoto.

Helmut Schwichtenberg — "Logic for exact real arithmetic"

Real numbers in the exact (as opposed to floating-point) sense can be given in different formats, for instance as Cauchy sequences (of rationals, with Cauchy modulus), or else as infinite sequences (streams) of (i) signed digits -1, 0, 1 or (ii) -1, 1, bot containing at most one copy of bot (meaning undefinedness), so-called Gray code (di Gianantonio 1999, Tsuiki 2002). We are interested in formally verified algorithms on real numbers given as streams. To this end we consider formal (constructive) existence proofs M and apply a proof theoretic method (realizability) to extract their computational content. We switch between different representations of reals by labelling universal quantifiers on reals x as non-computational and then relativising x to a predicate CoI coinductively defined in such a way that the computational content of x in CoI is a stream representing x. The desired algorithm is obtained as the extracted term of the existence proof M, and the required verification is provided by a formal soundness proof of the realizability interpretation. As an example we consider multiplication of reals.

Thomas Streicher — "Some recent results in Classical Realizability"

Classical realizability was developed by J.-L.Krivine the last 20 years. We give an introduction to this this theory and describe some recent results:

  1. By a result of van Oosten and Zou (2016) classical realizability models can be characterized as booleanizations of relative realizability models.
  2. We show that there are classical realizability models where dependent choice is realized via a kind of bar recursion. We discuss the possibility of refuting dependent choice in some classical realizability models.