A Problem Related to Quine's NF

Chad E Brown (Click here for slides from my talk at the CAMELEON meeting held at Cambridge in April 2008.)

A long standing open question is whether or not Quine's NF (New Foundations) is consistent (relative to ZFC). Two good sources for information about Quine's NF are Robert Holmes' New Foundations home page and the Stanford Encyclopedia of Philosophy page. My interest in Quine's NF started when Thomas Forster gave a couple of talks at Carnegie Mellon when I was a student there.

Ernst Specker proved models of NF correspond to models of type theory with a certain (unusual) properties. In my book I use logical relations to construct unusual models of simple type theory where versions of Cantor's theorem fail. I conjecture that one could use a similar logical relations construction to obtain a model of NF. Below we describe conditions on four mathematical objects and claim that if one can find four objects satisfying these conditions, then one obtains a model of NF (though we won't explain how here). It is possible that the conditions are inconsistent (even if NF is consistent). We also give formal versions of the conditions in the syntax of my simple proof term check simptcheck written in OCaml.

The Four Objects and Their Preconditions

The four mathematical objects are a set A, a collection B of subsets of A, a collection R0 of functions from A to A, and a function π from A to B. B should contain the empty set and A, be closed under complements and binary unions. π should be a bijection. R0 should contain all constant functions from A to A.

The setup in simptcheck notation.

A is a set. A positive solution to the problem will give a definition for A, so we declare it as a definition, without giving its defining term:

B is also a set that should be defined. We also must prove that B is a subset of the power set of A

R0 is a further set that should be defined. We must prove every member of R0 is in the set of functions from A to A.

Finally π is a function that should be defined. The function should send members of A to members of B.

Next we turn to further preconditions on these objects.

The empty set and A should be in B. Also, B should be closed under complements and binary union.

π should be bijective (that is, injective and surjective).

R0 should contain all constant functions.

Defining the Higher Type Domains

The set A will be used to interpret the base type (lowest type) 0. Let D0 be A (but in the simptcheck version we will always simply use A). The set R0 is an A-ary relation on A. We need to interpret the higher-types 1, 2, 3 and 4. Each type n+1 corresponds to sets of elements of type n. We will define each D(n) as well as an A-ary relation R(n) as follows:

D(n+1) = {X⊆D(n)|∀g∈ R(n) {x∈ A| g(x) ∈ X}∈ B}

R(n+1) = {G:A→ D(n+1)|∀g∈ R(n) {x∈ A| g(x) ∈ G(x)}∈ B}

In simptcheck notation:

Lifting π to the higher types

We need to lift π to the higher types in an ∈-preserving way. We do this by defining π1:D1→ P(D1) to be direct image of π and π2:D2→ P(D2) to be direct image of π1.

π1(X) = {π(x)|x ∈ X}

π2(W) = {π1(X)|X ∈ W}

In simptcheck notation:

Ensuring D1 is B

The idea behind the construction is to define D1 in such a way that D1 will be equal to B. In that case, π will be a bijection from D0 onto D1. We can prove D1=B given two conditions.

(A) For g∈ R0 and X∈ B, g^-1(X)∈ B.

(B) The identity function is in R0.

We want π1:D1→ D2 and π2:D2→ D3.

Two conditions will guarantee this:

(C1) For G∈R1 and X∈B, {x∈ A|∃ y ∈ X (G(x) = π(y))}∈B.

(C2) For k∈R2 and W∈D2, {x∈ A|k(x) ∈ π2(W)}∈B.

We want π1:D1→ D2 and π2:D2→ D3 to be surjective.

Two conditions will guarantee this:

(D1) For W∈ D2, we have {x∈ A|π(x)∈ W}∈ B

(D2) For Z∈D3, we have {X∈D1|π1(X)∈ Z}∈D2.

Ensuring Comprehension

To ensure comprehension, we can either ensure equality at types 0,1,2,3 and 4 are realized or that equality is realized at type 0 and the universal quantifier is realized at types 0,1,2 and 3.

Equality at type n corresponds to the following condition:

(En) For g,h∈ R(n), {x∈ A|g(x) = h(x)}∈ B.

Universal Quantification at type n corresponds to the following condition:

(Πn) For G∈ R(n+1), {x∈ A|G(x) = D(n)}∈ B.

We will consider two different versions of the problem. In both versions we include the condition (E0).

In the first version nflr1-claims we include the condition (E1)-(E4):

In the second version nflr2-claims we include the condition (Π1)-(Π4):

Resolving the Problem Using Simptcheck

The background knowledge necessary is in the file zfc-1-claims. This file contains the axioms of ZFC set theory and building up the basic theory of ordered pairs, functions, etc. The proofs are not included in zfc-1-claims and we do not need to check these proofs to resolve the problem. So, we want Simptcheck to follow processing zfc-1-claims by processing the file accept, directing Simptcheck to believe every claim made to that point. After processing zfc-1-claims and accept, Simptcheck should process one of the two versions of the problem given on this page. These are given in the files nflr1-claims and nflr2-claims.

After downloading the relevant files, and installing simptcheck, you should be able to check the setup.

To check the first version:

To check the second version:

Both versions report that there are four missing definitions (A, B, R0 and π) and 21 open claims.

A Positive Resolution

Let's focus on the first version: nflr1-claims.

A positive resolution of the problem would consist of a file nflr1-soln giving definitions of A, B, R0 and π and proof terms for the 21 open claims. We could use Simptcheck to check this is a solution as follows: simptcheck -r zfc-1-claims accept nflr1-claims -s nflr1-soln

If the solution is complete and correct, Simptcheck will exit with status 0. Otherwise, it exits with status 1.

A positive resolution to the problem would be very important because it would yield a model of Quine's NF.

A Negative Resolution

A negative resolution to the problem would prove that there are no values of A, B, R0 and π satisfying the conditions. This does not mean NF is inconsistent. It only means this approach cannot yield a model of NF.

A negative resolution to the first problem would be a file nflr1-neg which treats A, B, R0 and π as constants and the 21 claims as axioms and concludes with an inconsistent document item which gives a proof of false.

We could use Simptcheck to check a proof of inconsistency as follows:

If the proof of inconsistency is correct, Simptcheck will exit with status 0. Otherwise, it exits with status 1.

If you have a formal solution...

feel free to send it to me at .