PohlersFest
 
at the
 
WWU Institute for Mathematical Logic


On the occasion of Wolfram Pohlers' retirement the Institute for Mathematical Logic in Münster sponsored a colloquium and a workshop which took place July 17-19, 2008. For the colloquium, we gratefully acknowlegde financial support from the University of Münster, from the DVMLG, and from Springer-Verlag.

Festschrift

A Festschrift will appear in 2010 in the ontos series in mathematical logic under the title Ways of Proof Theory, edited by Ralf Schindler.

  • Festschrift (.pdf)

    Schedule

    The the colloquium took place in our lecture hall M 1 on Friday afternoon, July 18, 2008, and the workshop took place place in our lecture halls M 3 and M 5 on Thursday afternoon, Friday morning, and Saturday, July 17-19, 2008.

    Colloquium

    Location: Lecture hall M 1, WWU Math and Computer Science Dept, Einsteinstr. 62.
    Date: July 18, 2008.

  • 15:00 Address of welcome by the Rector of the University of Münster, Prof. Dr. Ursula Nelles
  • Address of welcome by the Chairman of the Mathematics and Computer Science Department of the University of Münster, Prof. Dr. Joachim Cuntz
  • Laudatio by Prof. Dr. Justus Diller
  • Juggling group (Hochschulsport)
  • 15:30 -- 16:20 Solomon Feferman (Stanford University, USA): The proof theory of classical and constructive inductive definitions: A forty year saga.
  • 16:20 -- 17:15 Break
  • 17:15 -- 17:55 Michael Rathjen (University of Leeds, UK): The emergence of infinitary impredicative proof theory.
  • 17:55 --18:00 „Hörsaal in Bewegung“ (Hochschulsport)
  • 18:00 -- 18:40 Arnold Beckmann (Swansea University, UK): Proof theory and weak arithmetics.

    Workshop

    Building upon the tradition of "Proof Theory: Workshop on Logic, Foundadional Research, and Metamathematics (Workshop on Proof Theory 2003)" which was held Oct 9-11, 2003 (cf. Annals of Pure and Applied Logic Vol. 136, Issues 1-2 (Oct 2005), pp. 1--218), the Institute for Mathematical Logic in Münster sponsored a proof theory workshop which took place July 17-19, 2008. For the workshop, we gratefully acknowledge financial support from the DFG.

    List of speakers and schedule

    The workshop took place on Thursday afternoon, Friday morning and Saturday, July 17-19, 2008.

    Thursday, July 17, 08. Location: Lecture hall M 3, WWU Math and Computer Science Dept, Einsteinstr. 62.

  • 16:00 -- 16:30 WELCOME COFFEE
  • 16:30 -- 17:10 Lev Beklemishev (Moscow), "Kripke models for provability logic GLP." Abstract: A well-known polymodal provability logic GLP introduced by G. Japaridze is complete w.r.t. the arithmetical semantics where modalities correspond to reflection principles of restricted logical complexity in arithmetic. This system plays an important role in some applications of provability algebras in proof theory. However, an obstacle in the study of GLP is that it is incomplete w.r.t. any class of Kripke frames. We provide a complete Kripke semantics for GLP. First, we isolate a certain subsystem J of GLP that is sound and complete w.r.t. a nice class of finite frames. Second, appropriate models for GLP are defined as the limits of chains of finite expansions of models for J. We prove a soundness and completeness result for GLP w.r.t. such expansions and obtain some standard corollaries such as the Craig interpolation property and the fixed point property. The techniques involves unions of n-elementary chains and inverse limits of Kripke models. All the results are obtained by purely modal-logical methods formalizable in elementary arithmetic.
  • 17:20 -- 18:00 Wilfried Buchholz (München), "(Co)recursion and notations for infinitary derivations."

    Friday, July 18, 08. Location: Lecture hall M 5, WWU Math and Computer Science Dept, Einsteinstr. 62.

  • 9:00 -- 9:40 Tim Carlson (Columbus, OH), "Progress on Patterns of Embeddings."
  • 9:40 -- 10:00 BREAK
  • 10:00 - 10:40 Laura Crosilla (Leeds), "Explicit Constructive Set Theory I." Abstract: We present a constructive set theory with operations in the style of Feferman's operational set theory. The set theory combines an extensional notion of set together with an intensional notion of operation and can also be seen as a bridge between constructive set theory a' la Aczel and Feferman's explicit mathematics. In previous joint work we introduced an operational extension, COST, of Aczel's CZF, which resembled as much as possible this set theory. In particular, it had implicit principles of collection. We here introduce a fragment, EST, of COST characterised by its being fully explicit. In this first talk we shall present the theory EST in some detail and show some of its key features.
  • 10:50 - 11:30 Andrea Cantini (Firenze), "Explicit Constructive Set Theory II." Abstract: We present a constructive set theory with operations in the style of Feferman's operational set theory. The set theory combines an extensional notion of set together with an intensional notion of operation and can also be seen as a bridge between constructive set theory a' la Aczel and Feferman's explicit mathematics. In previous joint work we introduced an operational extension, COST, of Aczel's CZF, which resembled as much as possible this set theory. In particular, it had implicit principles of collection. We here introduce a fragment, EST, of COST characterised by its being fully explicit. In this second talk we shall address the proof-theoretic strength of EST.
  • 11:30 -- 12:00 BREAK
  • 12:00 - 12:40 Gerhard Jäger (Bern), "Operations and Sets."

    Saturday, July 19, 08. Location: Lecture hall M 5, WWU Math and Computer Science Dept, Einsteinstr. 62.

  • 9:00 -- 9:40 Reinhard Kahle (Coimbra), "The Universal Set and Diagonalization." Abstract: We summarize some results about sets in Frege structures (a first order truth theory over applicative theories). The resulting set theory admits the definition of the universal set. For this reason, we discuss the treatment of diagonalization in this context.
  • 9:40 -- 10:00 BREAK
  • 10:00 - 10:40 Robert Lubarsky (Boca Raton, FL), "ITTM Oracles for Well-Foundedly Many Convergence Questions." Abstract: Several different ways of iterating infinite time Turing machines will be described, some of which have theories very different from the non-iterated version. Some preliminary results will be presented, as well as some open questions.
  • 10:50 - 11:30 Arnon Avron (Tel-Aviv), "Syntactic Safety and Predicative Set Theory." Abstract: We suggest a new basic framework for the Weyl-Feferman predicativist program by constructing a formal predicative set theory PZF which resembles ZF. The basic idea is that the predicatively acceptable instances of the comprehension schema are those which determine the collections they define in an absolute way, independent of the extension of the "surrounding universe". This idea is implemented using syntactic safety relations between formulas and sets of variables. These safety relations generalize both the notion of domain-independence from database theory, and Goedel's notion of absoluteness from set theory. The language of PZF is type-free, and it reflects real mathematical practice in making an extensive use of statically defined abstract set terms. Another important feature of PZF is that its underlying logic is ancestral logic (i.e. the extension of first-order logic with a transitive closure operation).
  • 11:30 -- 12:00 BREAK
  • 12:00 - 12:40 Helmut Schwichtenberg (München), "Computational content of proofs." Abstract: We consider logical propositions concerning data structures. If such a proposition involves (constructive) existential quantifiers in strictly positive positions, then -- according to Brouwer, Heyting and Kolmogorov -- it can be seen as a computational problem. A (constructive) proof of the proposition then provides a solution to this problem, and one can machine extract (via a realizability interpretation) this solution in the form of a lambda calculus term involving recursion operators, which can be seen as (and translated into) a functional program. We concentrate on the question how to control at the proof level the complexity of the extracted programs.
  • 12:40 -- 15:00 LUNCH BREAK
  • 15:00 -- 15:40 Monika Seisenberger (Swansea), "New ways of extracting algorithms from proofs." Abstract: Program extraction from proofs is a method to produce provably secure algorithms. In this talk we concentrate on the extraction of algorithms from classical and coinductive proofs which (1) leads to new algorithms and (2) requires less formalisation effort than the traditional specify-implement-verify method.
  • 15:50 -- 16:30 Thomas Strahm (Bern), "Primitive recursive selection functions for existential assertions over abstract algebras" (joint work with with Jeffery I. Zucker). Abstract: We generalize to abstract many-sorted algebras the classical proof-theoretic result due to Parsons, Mints and Takeuti that a Pi-2 assertion provable in Peano arithmetic with existential induction, has a primitive recursive selection function. This involves a corresponding generalization to such algebras of the notion of primitive recursiveness. The main difficulty encountered in carrying out this generalization turns out to be the fact that equality over these algebras may not be computable, and hence atomic formulae in their signatures may not be decidable. The solution given here is to develop an appropriate concept of realizability of existential assertions over such algebras, generalized to realizability of sequents of existential assertions. In this way, the results can be seen to hold for classical proof systems.
  • 16:30 -- 17:00 BREAK
  • 17:00 -- 17:40 Stan Wainer (Leeds), "Pointwise Induction and Slow Growing Bounds." Abstract: Formulating Arithmetic with a "pointwise" or (in the sense of Nelson) "predicative" induction, requires two kinds of variables, analogous to the normal/safe variables of Bellantoni-Cook but here called input/output. The resulting theory EA(I;O) has only sufficient strength to prove totality of the elementary functions, with polynomial time occuring at the level of Sigma-1 induction, and is interesting because of its strong analogies to PA and because the provable "transfinite" inductions (below epsilon-0) are now actually finite but uniformized by an ordinal in such a way that they are enough to prove the existence of the slow-growing hierarchy, but nothing more. These issues (first developed by Leivant 1995 in a somewhat different context), and the first steps of an extension to a predicative hierarchy of theories over EA(I;O), will be described briefly. As well as that of Leivant on various styles of ramified theories, the work described here is due to a succession of Ph.D. students at Leeds, as well as, significantly, Marc Wirz (Ph.D. Bern, 2005).


    Contact: Ralf Schindler, rds@math.uni-muenster.de