Fraenkel-Mostowksi set theory gives a model of substitution as well as names

Murdoch Gabbay, Heriot-Watt University

In my thesis I and Andrew Pitts gave a semantic model of alpha-equivalence based on set theory. I will show, using only elementary constructions, how this model extends to a semantic model of *substitution*. This turns the set-theoretic universe into a powerful generalisation of syntax, which raises intriguing possibilities for denotations of rewriting and logic. Further details can be found on my webpage www.gabbay.org.uk