Re: Uncountable sets in CZF?

From: KRamsay (kramsay_at_aol.com)
Date: 09/07/04 

Date: 07 Sep 2004 16:16:40 GMT

In article <cgkfng$abo$1@bunyip.cc.uq.edu.au>, D.McAnally@i'm_a_gnu.uq.net.au
(David McAnally) writes:
|The Platonic attitude that there is exactly one set R of real numbers is
|not fully appropriate.

I disagree. Even while wearing my constructivist hat I still
disagree.

If you're going to adopt the attitude that there isn't one, which is
up to you, you still are left with the fact that as far as ZF is
concerned, there exists a unique set R of real numbers. So if you're
in the middle of doing some reasoning inside ZF, your reasoning should
respect that. If you are not in the middle of doing some reasoning
based on ZF, then a few words about what you are doing instead might
be in order.

I think trying to think of the reals as not being unique can easily
lead to confusion if you don't carefully partition such beliefs off
from the mathematics one is trying to do, if it's in a system that
regards the reals as being unique. If there's some alternative
metatheory in which the unique existence of R is not a theorem, but
the results from model theory you want to use are, it should be named.

|One cannot assume that there is exactly one set R
|that must be common to all models of ZF,

Of course.

|or that models of ZF are flawed
|on the basis that R can be altered by taking a generic extension.

It depends on what you mean by "flawed".

Certainly it's possible for a model of ZF to have the real line as
its R. (If you like, think of it as a theorem of ZF. ZF doesn't
have a theorem saying there are standard models of ZF, but adding an
assumption such as the existence of a measurable cardinal, then there
exists a model M of ZF where the set of reals relative to M is R.)
Such a model might be considered more perfect.

In article <cgfu52$uev$1@bunyip.cc.uq.edu.au>, D.McAnally@i'm_a_gnu.uq.net.au
(David McAnally) writes:
|For myself, the easiest way to understand generic extensions is through
|Boolean-valued models.

Nice of you to go to the trouble of explaining that in your posting.
It looks like you tersely covered a good fraction of the key points of
the development of boolean-valued model as it's done in textbooks.

A Boolean-valued model M^G can be arranged to behave the way you
describe; we can wind up with an element f in M^G such that
|f:Z^->R^ is a bijection| = 1, where Z^ and R^ are the counterparts
of Z and R in M^G, although R^ is not what M^G considers to be R. This
f is essentially a function from ZxR to G. The most obvious choice
of f in this particular case is symmetrical under permutations of Z
and permutations of R (which both act on G).

The model can get away with thinking of "for each n, there exists an
r such that f(n)=r" as having a truth-value of 1 because the value of
"there exists an r such that f(n)=r" is the least upper bound of the
values of "f(n)=r" ranging over all r in R.

I think the problem arises when you try to apply the equivalence of
the Boolean-valued approach (which doesn't need to construct an actual
model of ZF) with a forcing approach that does.

In article <cgfun1$197$1@bunyip.cc.uq.edu.au>, D.McAnally@i'm_a_gnu.uq.net.au
(David McAnally) writes:
|A set G (not necessarily an element of V) is called a generic set if
|
| (1) G is a subset of F (i.e. all the elements of G are forcing
| conditions),
|
| (2) if p is an element of G, then any condition q weaker than p
| is an element of G,
|
| (3) if p and q are elements of G, then p and q are compatible,
|
| (4) if D is an element of V and D is a dense set of conditions,
| then G and D have nonempty intersection, i.e. G intersects
| every dense subset of F.
|
|For all x in V^B, define i_G(x) by induction on x by
|
| i_G(x) = { i_G(y) : y in dom(x), G intersects x(y) },
|
|and define V[G] to be the class with elements i_G(x) for x in V^B.

I wish you hadn't chosen to use the letter "V" for your model, since
V is the usual notation for the class of all sets. It requires a little
care to apply the construction to a proper class, but it can be done.
One useful trick is to realize that when we're working with proper
classes, we're really dealing with the predicates that define them.
So with V, really we're working with the predicate that's always true,
like 0=0.

If we apply this process to V, V^G can be a boolean-valued model
that fails to satisfy various statements true in V. If we reduce back
to a 0-1-valued model using such a mapping i_G, though, we go right
back to V. It doesn't leave us with any new elements than what we
started with.

In what sense are none of the elements new? In the sense that they
are in V, i.e. that 0=0. That's just a matter of definition. It's not
a metaphysical claim about "the real world of sets" or anything. The
whole discussion still can be regarded as an informal version of an
argument to be formalized in the language of ZF.

|Then V[G] is the smallest model of ZFC which contains V as a submodel and
|contains G as an element. V[G] has the same ordinals as V, and the same
|constructible sets as V.

In the case where we use V to mean the class of all sets, G already
was an element of V.

|For a formula \phi(x_1,...,x_k) with free variables x_1,...,x_k, and for
|elements y_1,...,y_k, of V^B, V[G] satisfies \phi(i_G(y_1),...,i_G(y_k))
|iff there exists a condition p in G such that p forces \phi(y_1,...,y_k).

In our main example, all conditions force f to be a bijection, but
i_G(R^)=R and i_G(Z^)=Z, and there is no bijection between Z and R.

I believe there is a problem with preserving quantifiers. When we are
evaluating a formula with a quantifier in V^B, we take the least upper
bound (for existential quantifiers) or the greatest lower bound (for
universal quantifiers). For this to be preserved under reduction to
a 0-1-valued model, it needs to be the case that when each member of
the set of elements of B whose greatest lower bound we are taking is
in the filter, then so is their greatest lower bound.

|Define G' in V^B by dom(G') = { \hat p : p in F }, and G'(p) = e(p) for
|all conditions p in F, then ||G' is a generic set|| = 1, and i_G(G') = G.
|It follows that if ZFC is consistent, then the existence of a generic set
|is consistent with ZFC.
|
|The connection between generic ultrafilters and generic sets is given as
|follows.
|
|If G is a generic set, then
|
| U = { A a regular open set in F : A intersects G }
|
|is the corresponding generic ultrafilter, and V[U] = V[G].
|
|If U is a generic ultrafilter, then
|
| G = { p in F : e(p) in U }
|
|is the corresponding generic set, and V[G] = V[U].

I think it's only the case that we get back a 0-1-valued model of ZF
satisfying the sentences whose values in V^B lie in U, if some other
condition is satisfied. Perhaps we need to use Lowenheim-Skolem to
cut down to a countable model, like Cohen did in his original forcing
papers.

Keith Ramsay

Relevant Pages

  • Re: The infintely small number b
    ... for that open set D, and they are not in R according to you. ... We call some l a lower bound of some P ... over the reals, so m is real. ... This proves that there exists a quality of the real ...
    (sci.math)
  • Re: The infintely small number b
    ... for that open set D, and they are not in R according to you. ... We call some l a lower bound of some P ... Assumption A) the inclusive lower bound l of P exists: ... over the reals, so m is real. ...
    (sci.math)
  • Re: .999... = 1
    ... > lower bound for S. The completeness axiom is this: ... If S is a set of reals and S is ... rational can be approached by a sequence of rationals that approach ... I take to be a particular way of 'approaching arbitrarily close'), ...
    (sci.logic)
  • Re: .999... = 1
    ... We say b is a lower bound for S if b <= x for every x ... If S is a set of reals and S is ... If S has a strictly positive lower bound ... >need to learn these theorems anyway. ...
    (sci.logic)