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

## Reflection in sheaf modelsAdd 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, 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. |
## Other listsType the title of a new list here Electromagnetic Communications and Sensing Research Seminar Series Lab Lunch## Other talksQuantum simulations using ultra cold ytterbium Modelling uncertainty in image analysis. Ultrafast, all-optical, and highly efficient imaging of molecular chirality Sylow branching coefficients for symmetric groups Extending the Lax type operator for finite W-algebras TBC |