Proof Theory in Lisbon

A one-day workshop

Date and venue

19 July 2013, in the room A2-25 of

Instituto para a Investigação Interdisciplinar

Avenida Professor Gama Pinto, 2

1649-003 Lisboa

Three-part lecture
Jean-Louis Krivine (Université Paris 7, CNRS): Models of ZF obtained by classical realizability

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 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.

Other speakers
Benno van der Berg (Utrecht University): Herbrand realizability

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").

Ali Enayat (University of Gothenburg): A new proof of Tanaka's self-embedding theorem

We present a new proof of a theorem of Kazuyuki Tanaka, which states that every countable nonstandard model of WKL0 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 WKL0 among countable models of RCA0.

Fernando Ferreira (Universidade de Lisboa): A new computation of the Σ1-ordinal of KPω

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-Π11 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ω.

Ulrich Kohlenbach (Technische Universität Darmstadt): Fluctuations, effective learnability and metastability in analysis

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).

João Rasga (Technical University of Lisbon): Preservation of Craig interpolation by the product of matrix logics

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 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.


VIP Executive Zurique

VIP Inn Berna

Alif Campo Pequeno

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


Fernando Ferreira

Jaime Gaspar


Fundação para a Ciência e a TecnologiaCentro de Matemática e Aplicações Fundamentais