Sergei
Tupailo
(Tallinn)
Consistency of Strictly Impredicative NF
An instance of Stratified Comprehension
∀x1…∀xn∃y∀x
(x∈y ↔ φ(x,x1,…,xn))
is called strictly impredicative iff,
under minimal
stratification, the type of x is 0. 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.
This work was done, in the main part, during author's visiting
appointment at Stanford last academic year, and finally reported to an "NF in the
Bay Area" conference, Stanford University, June 25-27, 2008.