Some informal notes on forcing in NF and NFU

1.  The forcing construction in NFU

Let <= be an s.c. partial order with domain P (and let >= be its
converse).  Since we need infinite s.c. partial orders, we need to
assume AxCount; this seems harmless, since AxCount is obviously true
:-)

For p,q in P, I write p <= q when q gives more information than p.  This
may be the reverse of the standard convention.

I understand forcing constructions by thinking about Kripke models of
intuitionistic logic.  There is a difference in the treatment of names
of objects:  all names that we will ever use are present at the top
level, and the question as to whether two names are equal may be settled
differently in different "possible worlds" (once settled, it remains
settled, of course).  Also, of course, we need our logic to be classical,
so we take care that our connective definitions and the semantics of
our atomic sentences work correctly.  All of this is true of standard
forcing techniques; there is no novelty about any of this!

It is possible to do forcing in NFU by simulating the standard forcing
constructions in the interpretation of (a fragment of) Zermelo set theory
in the isomorphism classes of well-founded extensional relations.  The same
simulation can be carried out in NF, but creates a lot of urelements.

The development here takes a different tack, though for NFU the results 
one can prove are not different.  The advantage for NFU is philosophical;
the construction is simple and natural in the NFU context.  I defined this
construction while I was on sabbatical in Cambridge; it is modelled on
Marcel's weak extensional collapse of (NF - extensionality) to NFU.

We define a special class of subsets of P, which we can think of as
"classical truth values".  RO(P) = the set of all subsets A of P
such that 

	i.  for any p in A and q >= p, q is in A.

        ii.  If p in P has the property that for every q >= p, there is
        r >= q such that r is in A, then p is in A (this ensures that
        we have a "classical" truth value).

We interpret all sets in our original model of NFU as functions from V
to RO(P), by defining A[x] as the unique a in RO(P) such that (x,a) is
in A, or as the empty set (which is an element of RO(P)) if there is
no such unique a.  Note that the relative type of A is one higher than
the relative type of x in A[x].  (It is important to note here that I
use a type-level pair (definable in NF, provably existing in
NFU + Infinity + Choice), so the type of a function is one higher
than its arguments and values, instead of three higher).

We can now interpret every element of our universe as a "name"; if p
is an element of A[x], we would like to say that p forces "x is in A".
But we can't, for reasons we will see shortly.

We begin by defining equality of names.  This is defined exactly in
line with the intuition above:  p in P forces "A = B" (we write this
p |- A = B) just in case for all x, p is in A[x] if and only if p is in B[x].
Notice that the types of A and B are the same in this definition, and
the type of p is two types lower (but is "adjustable" because P is s.c.).

Now we see the problem.  The identity criteria for "elements" x of A
under the condition p (objects x such that p is in A[x]) are the
identity criteria of the original model of NFU, not the new identity
criteria of the forcing interpretation.  The obvious way to change
this (which is used in standard set theory) would involve induction on
membership, which is impossible here.  What we do instead, following
Marcel's idea of "weak extensional collapse", is treat "names" which
do not respect the identity criteria of the forcing interpretation as
urelements.

We say that p |- set(A) (p forces "A is a set") if and only if for
every q >= p, x such that q is in A[x] and y such that q |- x = y,
it is also the case that q is in A[y].

This says that if x is intuitively an "element" of A under condition q
at least as strong as p, and q forces x=y, then y is also intuitively an
"element" of A under condition q.

This definition is only stratified because P is s.c.  In q \in A[x], q
is one type lower than x, while in q |- x=y, q is two types lower than
x.  But the fact that P is s.c. allows the type of q to be adjusted
freely.

Now we can define our official membership relation:

(p |- x is an element of A) iff p is an element of A[x] and p |- set(A).

Notice that x is one type lower than A, just as in "x is an element of
A".

Additional details:

define p |- x & y as p |- x and p |- y

define p |- (Ax . phi) as (Ay. p |- phi[y/x])
(this is different from the usual definition in Kripke
models because all names are present in all worlds).

define p |- ~phi as (Aq >= p. ~(q |- phi))

Then define all other connectives using their definitions from these
connectives in _classical_ logic.

Notice that this is only defined for concrete sentences (with instantiations
of variables by arbitrary names); |- is certainly not a set!

Everything has classical semantics (is equivalent to its double
negation) because atomic sentences have classical semantics (due to
the role of RO(P) in the definitions) and we use only classical
connectives and quantifiers.

Equality has the right logical properties because all atomic sentences
satisfy the correct logical properties for equality; the rest follows
by induction on the complexity of sentences.

For standard reasons, if p |- phi and psi is deducible in classical
logic from phi, then p |- psi.

One comment: in the absence of choice (as in NF), there may be no name
which witnesses an existential statement true at a condition p --
however, in such a case there will be a dense set of conditions
stronger than p at which there is a name witnessing the statement.
This appears to be harmless.  It does not affect the validity of
comprehension axioms, nor does it affect the validity of classical logic
in the forcing interpretation.

Another comment:  The "truth values" of unstratified statements
may be proper subclasses of P.  That is, for some unstratified sentence
phi, the class of all p such that p |- phi may not be a set.  The Axiom
of Small Ordinals would preclude this, but the phenomenon does not seem
to be harmful.  It does mean that I feel freer to work with P instead
of the Boolean algebra RO(P), as is mathematically more convenient 
in forcing constructions.  Stratified sentences will have "truth values"
in RO(P).

Weak extensionality holds in the forcing interpretation; this should
be clear from the definitions.  To see that comprehension holds, let
phi be stratified.  A name for the set of x such that phi is the
set of all pairs (a,A) such that A is the set of all conditions p
such that p |- phi[a/x].  A exists because the stratification conditions
for p |- phi[a/x] are the same as those for phi; it belongs to RO(P)
by considerations outlined above.

I've worked my way through the standard proof of the independence of
CH, and it all goes as usual.  Of course, the construction of
analogies between ordinals and cardinals in the underlying model and
ordinals and cardinals in the forcing interpretation and the statement
of assertions such as "ccc forcing relations preserve cardinals" based
on these analogies look a little different (but not much different).

I got this far in Cambridge, though I looked closely at the details
of the standard forcing proof for CH only recently.

Forcing in NF

This forcing construction, if applied in NF, will create urelements
(there will be names which do not respect equality).  The big surprise
is that on close examination it turns out that the model of NFU
obtained after forcing on P has no more urelements than sets, and so
can be converted back into a model of NF (using "permutation
techniques" -- though the map used is not really a permutation!  The
theorem, due to Boffa, is that if one has a bijection f from V onto
P(V) in a model of NFU one can redefine membership: x E_new y is
defined as x E f(y), and this will give a model of NF).  Statements
whose independence is proved by forcing arguments are invariant under
"permutation techniques" (even when generalized), so we have forcing
for NF as well, which is a breakthrough!

The old approach to forcing could not do this -- it was clear that
there were many more urelements than sets in models built by forcing
on isomorphism types of well-founded extensional relations in NFU or
NF.

It is sufficient to show that there is an injection from the universe
into the set of sets in the forcing interpretation in NF.  The rest follows
by Schroder-Bernstein.

The construction is best explained by returning to the idea that under
condition p, a name A intuitively has as its "elements" the objects x
such that p is an element of A[x].  We had to abandon this intuition because
it didn't respect equality (for some names A, p might force x = y
and we might have p in A[x] but not in A[y]).

We can recover this by exhibiting objects char(x) such that for all
conditions p, p |- char(x) = char(y) just in case x = y in the real
world; we then (speaking intuitively again) replace the "elements" of
each name A with their images under char to obtain a name of a set
uniquely determined by the general name A.  

char(x) is defined as the function which takes all elements of x to P
(which is an element of RO(P)) and all elements of y to the empty set
(which is also an element of RO(P)).  (Note that char(x) is at the
same relative type as x; this depends on the use of a type-level
ordered pair.)

The condition on char given above is easily seen to hold.  It does not
hold in NFU:  p |- char(u) = char(v) for any urelements u and v.

Now the idea is to turn an arbitrary name A into a set by replacing all
of its intuitive "elements" under all conditions with their images under
char, which will eliminate any conflicts with the notion of equality
in the forcing interpretation, because equality between char(x) and char(y)
under any condition coincides with equality between char(x) and char(y)
in the real world.

We define A' as the set of all (char(x),a) such that A[x] = a.

A' is not a set:  some objects y which are not images under char
are equal to some char(x) under some conditions, and these need to be
added:

for any name B define B* as the function taking each x to the set of
all conditions p such that for each condition q>=p, there is a
condition r>=q such that there is a y such that r |- x=y and r belongs
to B[y].

This is a general operation for fattening a name so that it respects
the equality of the forcing interpretation.

We take (A')* as the image of A under the injection we are trying to
construct.  It is clear that (A')* is a set.  We need to establish that
this is really a function (respects equality) and that it is an injection.
It is easy to see that p |- "A=B iff A'=B'" because A' is constructed from
A by replacing the "elements" of A with objects with precisely parallel
identity conditions.  To see that p |- "A'=B' iff (A')* = (B')*",
observe that nothing is an element of (A')* under a condition p without
being equal to a char(x) under that condition, and identity conditions
on char(x)'s are the same under all conditions:  it is safe to ignore
the stuff added in the fattening process.

If one forces on NF + AxCount with the extension (not inclusion)
partial order on well-orderings of proper subsets of the reals, one
obtains a model of NFU + AxCount + "the continuum can be well-ordered"
(the details require checking, but this is not hard -- POSSIBLE GAP --
I do _not_ see that this works; if aleph(c) has countable cofinality
things might not work!).  Then a permutation can be used to eliminate
the urelements (because there are no more urelements than sets) and
the process of constructing the permutation model will not affect the
truth of the invariant sentence "the continuum can be well-ordered".
This is a brand-new result which no previously available techniques
could touch.

More comments:

The forcing technique in NFU is _easier_ than the standard techniques
in ZFC (if one understands how to work in NFU, which is a big "if"!),
because it is not necessary to iterate the construction of names.  At
least, that's my immediate perception.  Quite the reverse was true of
the old technique with the detour through equivalence classes of
well-founded extensional relations: it was far nastier than the
technique in ZFC and obviously parasitic on it.

I have developed a "native" technique for symmetry arguments in NFU
(analogous to proofs of the independence of choice from ZFA).  This is
much more technical, and I haven't tried putting it together with the
forcing.

Is there a nice way to formulate forcing in NF so that no urelements are
ever created?

This technique is "boolean valued"; I don't make any effort to
collapse the space of conditions or "possible worlds".  In NFU +
Choice, one could use an ultrafilter to collapse the "multi-valued"
model to a 2-valued model; I don't see that this is really all that
helpful, as such models are very likely to be pathological in some way.
In NF, we can show consistency of enough choice to allow collapse of
any given forcing interpretation to a 2-valued interpretation.  I
don't see that the machinery of countable transitive models and
generic ultrafilters is natural to use in the NF context: it isn't
nearly as natural to think of models of NFU inside the world of NFU as
it is to think of models of ZFC inside the world of ZFC.

It would be nice to have separation for s.c. sets.  I asked Solovay
how strong NFU + AxCount + "every subclass of an s.c. set is a set"
might be.  This would ensure that the "truth values" of all sentences
were represented by sets.  It also gives such things as full math
induction.  Is it as strong as ZFC - power set + weakly compact?  Of
course, the Axiom of Small Ordinals works for this, but it would be
interesting if s.c. separation were weaker.

A possible problem:

This has nothing to do with the forcing technology -- I'm not sure how
to force the well-ordering of the reals in the absence of choice.  I have
heard rumors that this has been done, but I haven't got the details right.