An Instance of Stratified Comprehension; for all x(1) for all x there exists y for all a (a is an element of y <-> phi(x x1)); 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 Apparently this is a new subsystem of NF shown to be consistent The consistency question for the whole theory NF remains open (since 1937)
展开▼
