This talk will focus on a particularly nice construction of initial segments related to a Banach-Mazur game in arithmetically saturated models of Peano arithmetic. The intuition is that if an initial segment I of a model M is constructed in as general way as possible, with as little information being added, then the first order theory of the pair (M,I) should be determined in a comparatively straightforward way from the theory of M together with the closure properties of I. The initial segments constructed in this way are called generic and the construction takes place relative to some appropriate closure conditions chosen in advance: one can consider a generic initial segment closed under the primitive recursive functions, or an elementary generic initial segment.

In particular I shall report on recent work by the author and Tin Lok Wong on generic initial segments. In particular we will explain the notion of genericity and its relation to the Banach-Mazur game. The main theorem concerns a description of truth in the structure (M, I), where I is a generic cut of a model M of PA. This work relates to open questions raised by Roman Kossak on free cuts.

limit : (Nat -> Y) -> Y,

for a compact metric spaces Y, and

supremum : ([0,1] -> Real) -> Real

integral : ([0,1] -> Real) -> Real.

A generalised quantifier phi : (X -> R) -> R is called attainable if it has a selection function

e : (X -> R) -> X

i.e. if there exists a function e : (X -> R) -> X producing the point where the quantifier "attains its p-value" for any "predicate" p : X -> R

phi(p) = p(e(p)).

In the case of the existential quantifier, for instance, this is Hilbert's epsilon term. In the case of integration, the mean value theorem says that integration over C[0,1] has a selection function, i.e. for any p in C[0,1] there exists an x in [0,1] such that

integral(p) = p(x).

Hence, there must exist a function e : ([0,1] -> R) -> [0,1] such that

integral(p) = p(e(p)).

This talk aims to motivate the concept of selection functions and some associated constructions through simple concrete examples from Nash equilibrium (backward induction), fixed point theory (Bekic's lemma), algorithms (backtracking) and proof theory (bar recursion). Talk based on joint work with Martin Escardo.

*References:*

[1] Harvey Friedman, Some systems of second order arithmetic and their use, Proceedings of the
International Congress of Mathematicians (Vancouver, B. C., 1974), Vol. 1, Canad. Math.
Congress, Montreal, Que., 1975, pp. 235 - 242.

[2] Harvey Friedman, Systems of second order arithmetic with restricted induction, I & II (Abstracts),
Journal of Symbolic Logic 41 (1976), 557 - 559.

[3] H. Jerome Keisler, Nonstandard arithmetic and reverse mathematics, Bull. Symbolic Logic 12
(2006), no. 1, 100 - 125.

[4] H. Jerome Keisler, Nonstandard arithmetic and reverse mathematics, Bull. Symbolic Logic 12 (2006),
no. 1, 100 - 125. MR2209331 (2006m:03092)

[5] Stephen G. Simpson, Subsystems of second order arithmetic, Perspectives in Mathematical
Logic, Springer-Verlag, Berlin, 1999.

[6] Kazuyuki Tanaka, The self-embedding theorem of WKL0 and a non-standard method, Ann.
Pure Appl. Logic 84 (1997), no. 1, 41 - 49.

Its technical usefulness aside, why does the metatheorem work at all? Continuity is an issue; another one is (avoiding) choice. Neither gives a definitive answer, but the latter has shown the right direction. Working with completions defined without sequences has in fact revealed that completeness is even equivalent to the unique solution property. If not new, this is a characterisation of completeness for metric spaces custom-made for short proofs of the numerous basic theorems to which uniqueness is inherent. The Banach fixed point theorem and its applications (implicit functions, Picard-Lindeloef, etc.) are simple but characteristic examples.

We present the nu-lambda-mu calculus: an extension of Parigot's lambda-mu calculus achieving a direct correspondence with Gentzen's classical natural deduction. We equip the resulting calculus with a naturally non-confluent reduction relation, motivated by an intuitive semantics.

The reduction behaviour of the calculus is highly expressive, and able to encode those of popular alternatives in the literature. From a logical perspective, we can encode Urban's non-confluent cut elimination for classical sequent calculus. From a programming perspective, a delimited control operator arises naturally, which can be used to encode jumps, exceptions, loops etc.

We describe some recent work characterizing these problems in terms of a combinatorial principle about games; this is shown by translating first-order proofs in such a theory into large, uniform propositional proofs in a proof system where the soundness of the rules can be witnessed by a feasible strategy for reducing one game to another. We also show that this can be restated as a principle about local improvements of labellings of a large graph, and that this new principle can be extended naturally to characterize the provable NP search problems of "second-order" bounded arithmetic theories corresponding to PSPACE and EXP.

An important result in the area by de Jongh and Parikh states that every wpo can be extended to a linear order (on the same domain) which among all such linear extensions has a maximal possible order type. It turns out from results of de Jongh, Parikh, Schmidt and Friedman that such maximal order types are mathematical invariants which prove very useful for classifying the proof-theoretic strength of wpo'ness assertions. For example, a classic result by Friedman states that Kruskal's tree theorem is not provable in predicative analysis.

In our talk we present a new, short and very aesthetic formula which allows to describe a plethora of (old and new) results on maximal order types in a uniform way and we indicate related proof-theoretic applications. (Joint work with Michael Rathjen.)

Our long term research aim consists in classifying the strength of Friedman-Kriz style tree theorems which are based on a so called gap condition.

Anton Setzer Last modified: Fri Aug 28 20:32:02 BST 2009