Herbrand realizability

Photograph of Benno van den Berg

Benno van den Berg


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 also talk about a Dialectica variant of Herbrand realizability or its categorical aspects (a "Herbrand topos").
Tuesday 10th April 2012, 16:00
Board Room
Department of Computer Science