##### Personal tools
You are here: Home LFCS seminar: Murdoch Gabbay: Nominal techniques and the consistency of Quine's NF

# LFCS seminar: Murdoch Gabbay: Nominal techniques and the consistency of Quine's NF

— filed under:

What LFCS Seminar May 31, 2016 from 04:00 PM to 05:00 PM IF 4.31/4.33 vCal iCal

Abstract:

Naive set theory has one rule; naive sets comprehension:  If φ is a predicate, then {a | φ(a)} is a set (the ​set of ​a such that φ).

This is inconsistent by Bertrand Russell’s famous observation of 1901 that

​   {a | a ∉ a} ∈ {a | a ∉ a} if and only if {a | a ∉ a} ∉ {a | a ∉ a}​.

This is of course the famous "barber" example concerning the set of all barbers that do not shave themselves.​

Solutions proposed included Zermelo-Fraenkel set theory, simple type theory, and Quine’s New Foundations (NF).

NF works by restricting comprehension to stratifiable formulae; those in which variables can be assigned ‘levels’, which are natural numbers, such that if a ∈ b occurs and a has level n, then b must have level n+1. Russell’s example is ruled out because a ∈ a cannot be stratified.

Consistency of NF has been an open problem since it was proposed by Quine in 1937.

I will present a claimed proof of consistency for Quine’s NF, based on nominal techniques, and in particular based on novel interpretations of

* stratifiability as normalisability under a simple rewrite relation, and of

* universal quantification as a limit in nominal lattices and a variant of the characteristic ‘NEW’ quantifier familiar from nominal techniques.

I will try to explain my claimed proof, exhibiting it as ​flowing naturally from a new way of looking at the semantics of logic and computation which I have been developing now for several years​.

​​Technical proficiency in set theory or nominal sets will not be required to have a good time.

Courageous or reckless readers can access the raw maths here:

www.gabbay.org.uk/papers.html#conqnf

www.gabbay.org.uk/papers.html#semooc

www.gabbay.org.uk/papers.html#repdul