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


When 
May 31, 2016 from 04:00 PM to 05:00 PM 
Where  IF 4.31/4.33 
Add event to calendar 
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 ZermeloFraenkel 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