Derived Rules

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.