Personal tools
You are here: Home Events LFCS Seminars-Folder 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:

  • LFCS Seminar
When May 31, 2016
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Add event to calendar vCal


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:

Document Actions