Nominal Foundations of Mathematics

Murdoch Gabbay
Heriot-Watt University

2:15pm-3-15pm, 30 March 2016
EM G.44

Abstract

Nominal techniques take variable symbols as a primitive datatype — so the variable "x" is a primitive datum in a distinct (new) datatype structure. (Technically, "x" is an urelement in Fraenkel-Mostowski set theory.)

Variables are a determining feature of many (if not most) logics and calculi, so by understanding variables in new ways, we understand logics and calculi in new ways. And indeed, it turns out that astonishing richnesses of structure emerge which have been applied: in formal methods and mechanised theorem-proving, concurrency, rewriting, automata theory, and much more.

I have been applying these ideas to the foundation of mathematics itself. Specifically, I've studied three systems:

Using nominal models I have amongst other things given Stone duality constructions for first-order logic and the untyped lambda-calculus (an open problem), and also a claimed proof of the open problem of the consistency of Quine's NF.

The results are interesting in themselves, they have philosophical significance, and it is clear that the methods used in the proofs are general and interesting, and that the further possibilities are probably extensive.

I will endeavour to deliver an accessible — that's right: accessible, to the best of my ability! — guided tour of this material. Technical familiarity will not be required to have a good time.

Courageous or reckless readers can access relevant papers here:
http://www.gabbay.org.uk/papers.html#semooc
http://www.gabbay.org.uk/papers.html#repdul
http://www.gabbay.org.uk/papers.html#conqnf

A copy of the presentation is available at:
http://www.gabbay.org.uk/talks/20160330-hw.pdf