University of Birmingham > Talks@bham > Theoretical computer science seminar > Reflection in sheaf models

Reflection in sheaf models

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

If you have a question about this talk, please contact Paul Levy.

A sheaf model is given by interpreting logic in the topos of sheaves on a site. A reflection principle for such a model, M, says that, for formulae φ in some class of formulae φ is true in the sheaf model iff φ is true. In short, M ⊨ φ iff φ.

Sheaf models were first used, unwittingly, by Cohen to show the independence of the axiom of choice. Particular ‘topological’ sheaf models have also been used to show the relative consistency of various strongly non-classical Brouwerian principles, such as the continuity principle, “all functions ℝ → ℝ are continuous”.

We will briefly present this background and then show that some natural topological sheaf models satisfy a reflection principle for predicative formulae, φ, viz. M ⊨ “M ⊨ φ iff φ”. Such principles have philosophical significance, if we think of sheaf models as embodying the intuitionistic explication of mathematical meaning that Brouwer uses to justify his principles.

I plan to make this talk accessible to to a general audience without a deep knowledge of categories or logic, but I will touch briefly on some questions for specialists at the end of the talk.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.