Consistency of strictly impredicative NF

Sergei Tupailo

Centro de Matemática e Aplicações Fundamentais
Universidade de Lisboa

Thursday, 26 January 2012, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101


Slides from the talk [pdf]

Abstract: We present the following our main contribution into the consistency problem of NF:

An instance of Stratified Comprehension

   A x_1 ... A x_n E y A x (x in y <--> phi(x,x_1,...,x_n))

is called strictly impredicative iff, under stratification, x receives the minimal type. Using the technology of forcing, we prove that the fragment of NF based on strictly impredicative Stratified Comprehension is consistent. A crucial part in this proof, namely showing genericity of a certain symmetric filter, is due to Robert Solovay.

As a bonus, our interpretation also satisfies some instances of Stratified Comprehension which are not strictly impredicative. For example, it verifies existence of Frege natural numbers.

Apparently, this is a new subsystem of NF shown to be consistent. The consistency question for the whole theory NF remains open (since 1937).

Main reference:

S. Tupailo. Consistency of Strictly Impredicative NF and a little more... Journal of Symbolic Logic, v. 75, n. 4, 1326-1338, 2010.


Tarmo Uustalu
Last update 5.2.2012