19 July 2013, in the room A2-25 of
Instituto para a Investigação Interdisciplinar
Avenida Professor Gama Pinto, 2
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
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.
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 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.
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ω.
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:45–11:30||Benno van der Berg|
|14:00–15:00||Jean-Louis Krivine II|
|17:45–18:45||Jean-Louis Krivine III|
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.
VIP Executive Zurique
VIP Inn Berna
Alif Campo Pequeno
All these hotels are walking distance from Campo Pequeno metro station.