Derived Rules
- Date: Wednesday 14 March 2018, 14:00 – 15:00
- Location: Mathematics Level 8, MALL 2, School of Mathematics
- Type: Proofs, Constructions and Computations, Seminars, Pure Mathematics
- Cost: Free
Michael Rathjen, University of Leeds. Part of the proofs, constructions and computations seminar series.
Each partial combinatory algebra A gives rise to a set-theoretic realizability universe, V*(A), that amalgamates standard realizability with truth in the background universe V. If A is taken to be the first Kleene algebra, then this technique can be used to show that the disjunction and numerical existence property as well as closure under Church's rule hold for almost all (reasonable) intuitionistic set theories.
This result lends itself to the question whether other pcas could be usefully employed in ascertaining further derived rules. The talk will explore these possibilities.