*19 July 2013, in the room A2-25 of*

Instituto para a Investigação Interdisciplinar

Avenida Professor Gama Pinto, 2

1649-003 Lisboa

Classical realizability appeared as a method to extend the proof-program
correspondence to the whole of ZF set theory, even with DC (dependent choice). As a by-product, it gives completely new models of
ZF + DC, that we shall consider in these talks. The method of forcing is indeed a (very) particular case, that we shall avoid, of
course.

The principal tools are:

- The structure of
*realizability algebra*, which is a three-sorted variant of the well known*combinatory algebra*of Curry.

The*sets of conditions*used in forcing are degenerate cases of realizability algebra. - The ZF
_{ε}set theory, which is a conservative extension of ZF, with a new strong membership relation ε*which does not satisfy extensionality*.

The models of ZF obtained in this way are much more difficult to study
than forcing models: they are not extensions of the ground model, ordinals and even integers are not preserved and neither is the axiom of
choice. I shall explain what we already know about their structure. We shall look at some examples, which give some new relative consistency
results, with DC and ℝ not well ordered.

Up to now, there are few such results, even though the method is much more general than
forcing. The reason is, of course, that we do not yet understand sufficiently well the structure of these models.

In a joint paper with Eyvind Briseid and Pavol Safarik devoted to formal systems for nonstandard analysis, we introduced "Herbrand realizability", a new realizability interpretation. Although the original motivation came from nonstandard analysis, it can also be explained as a modification of Ulrich Berger's uniform arithmetic or Lifschitz' calculable numbers. The idea there is to have two types of quantifiers, one with computational content and one without, so as to have more control over how one extracts programs from proofs. One drawback (if one sees it that way) is that one is also forced to have two types of disjunction. This is precisely what is avoided in Herbrand realizability. If time permits, I will talk about its categorical aspects (a "Herbrand topos").

We present a new proof of a theorem of Kazuyuki Tanaka, which states that every countable
nonstandard model of WKL_{0} has a nontrivial self-embedding on a proper initial segment of itself. Moreover, the new proof has an
ingredient that yields a novel characterization of models of WKL_{0} among countable models of RCA_{0}.

We define a functional interpretation of KPω using Howard's primitive recursive tree
functionals of finite type and associated terms. We prove that the Σ-ordinal of KPω is the least ordinal not given by a closed
term of the ground type of the trees (the Bachmann-Howard ordinal). We also extend KPω to a second-order theory with
Δ_{1}-comprehension and strict-Π^{1}_{1} reflection and show that
the Σ-ordinal of this theory is still the Bachmann-Howard ordinal. It is also argued that the second-order theory is
Σ_{1}-conservative over KPω.

We discuss a hierarchy of quantitative forms of Cauchy statements of increasing strength (rates of metastability, effective learnability with effectively bounded mind changes, fluctuation bounds, rates of convergence) and provide general proof-theoretic metatheorems on the extractability of such data. We explain recent applications of proof mining to ergodic theory in terms of these results (partly joint work with Pavol Safarik).

The product of matrix logics, possibly with interaction, is shown to preserve a slightly relaxed notion of Craig interpolation. The result is established symbolically, capitalizing on the complete axiomatization of the product of matrix logics provided by their meet-combination. Along the way preservation of the metatheorem of deduction is also proved. The computation of the interpolant in the resulting logic is proved to be polynomially reducible to the computation of the interpolants in the two given logics. Illustrations are provided for classical, intuitionistic and modal propositional logics. The talk reports on joint work with Cristina Sernadas and Amílcar Sernadas.

09:30–10:30 | Jean-Louis Krivine I |

10:30–10:45 | Break |

10:45–11:30 | Benno van der Berg |

11:30–12:15 | Ulrich Kohlenbach |

12:15–14:00 | Lunch |

14:00–15:00 | Jean-Louis Krivine II |

15:00–15:45 | Fernando Ferreira |

15:45–16:00 | Break |

16:00–16:45 | Ali Enayat |

16:45–17:30 | João Rasga |

17:30–17:45 | Break |

17:45–18:45 | Jean-Louis Krivine III |

20:00 | Dinner |

If you intend to participate in the meeting, please send an e-mail message to Fernando Ferreira at tp.lu.cf@arierrefjf. There is no registration fee.

The Lisbon Portela Airport is served
by *metro* (underground, a ride costs 1.40€) and by taxis (a ride to the centre of Lisbon should cost around 10€). Assuming that you are
already in Lisbon, the best way to reach the venue is to take the *metro* and exit at
the station *Cidade Universitária*. You can find the network diagram here.

All these
hotels are walking distance from *Campo Pequeno* metro station.