University of Cambridge > > Category Theory Seminar > Toposes for modified realizability

Toposes for modified realizability

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact José Siqueira.

One aim of the theory of realizability toposes is to give a conceptual and semantic account of the various realizability interpretations one can find in the proof-theoretic literature. But there is no direct route which goes from a proof-theoretic interpretation to its “corresponding” topos. In fact, one quickly finds that one has to make some choices on the way. I will discuss some of the issues that come up when one tries to define a modified realizability topos. Recall that the proof theorist (Kreisel, Troelstra) will think of modified realizability as an interpretation of arithmetic in finite types which validates independence of premise and the axiom of choice for all finite types. In the literature (Van Oosten’s book, for instance) one can find a modified realizability topos, due to Grayson, but it does not validate the axiom of choice for all finite types. I will discuss two possible ways in which this can be fixed. If time permits, I may even discuss a fourth topos which also has some claim to being a topos for modified realizability. (Joint work with Mees de Vries)

This talk is part of the Category Theory Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity