ABM Meeting Spring 2018

Michael Bärtschi — "Uniform fixpoints and relatives in second order arithmetic"

With the help of an extension of the usual language of second order arithmetic, we will introduce a uniform version of the fixpoint axiom (FP). With ACA₀ as our base theory, we will discuss connections to uniform versions of (ATR), i.e., the axiom schema of arithmetic transfinite recursion, and embed the uniform theory UFP₀ into a subsystem of Kripke Platek set theory. Moreover, we will touch upon relations to systems of iterated fixpoints. In this context we will also consider additional axiom schemas for UFP₀.

Nils Köpp — "On representations of real numbers and how to (ab)use them"

We will discuss two representations of (constructive) real numbers, namely by cauchy-sequences and sd-code. Then we will see how to translate between the two representations and how this can be useful when trying to avoid complicated proofs.

Iosif Petrakis — "Interactions between a universe of types and its successor universe"

We present some results/remarks on the interaction between basic types in a universe U and their counterpart in the successor universe U'. We also explain how U and U' are used in a Yoneda-lemma formulation of Voevodsky's univalence axiom. This formulation is related to Jäger's question: "how one can understand the univalence axiom outside the type-theoretic framework?".

Kentaro Sato — "Hierarchy of Formula-classes in the Intuitionistic Second Order Setting"

In the context of intuitionistic function-based second order arithmetic, we consider a hierarchy of classes of second order formulae. As is well known, classically common Π-Σ type hierarchies do not work well in the intuitionistic context. Our hierarchy is a second order analogue of Burr's Theta-hierarchy, where the latter is defined in the first order context. With this hierarchy, we slice Brouwer's bar induction schema and consider the proof-theoretic strengths.

This is another talk based on the following joint-paper with T. Nemoto.

T. Nemoto and K. Sato, A marriage of Brouwer's Intuitionism and Hilbert's Finitism I: Arithmetic, to appear in JSL

Helmut Schwichtenberg — "The fan theorem for uniformly coconvex bars"

Proofs can have computational content, and the most direct method to extract it is via a realizability interpretation in the form given by Kreisel. After a short introduction into the subject we present a recent case study on Brouwer's fan theorem for uniform coconvex bars. As an application we prove a constructive version of the Heine-Borel Theorem, for uniformly coconvex coverings.

Franziskus Wiesnet — "Limits in the Signed Digit Representation of Reals"

We work with the signed digit representation of abstract real numbers, which roughly is the binary representation enriched by the additional digit -1. We consider an algorithm which takes a sequence of signed digit representations of reals and returns the signed digit representation of their limit, if the sequence converges. As an application we use this algorithm together with Heron's method to build up an algorithm which converts the signed digit representation of a non-negative real number into the signed digit representation of its square root.