Reflection in sheaf models

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

• Michael Fourman, University of Edinburgh
• Thursday 04 July 2013, 14:00-15:00
• UG10 Learning Centre.

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.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG10 Learning Centre
• computer sience

Note that ex-directory lists are not shown.