Abstract

The Substitution Rule is a central component of Doug Howe's elegant semantic pathway between Nuprl and set theory.
I will ask the audience to consider whether it might, in some cases, be interesting to run that rule in reverse.

The initial part of the talk will be an introduction to Howe's model, using singleton types, two different trees
that span the entire collection of singleton types, and an unobtrusive choice operator as stepping stones.