Re: Uncountable sets in CZF?

From: David McAnally (D.McAnally_at_i'm_a_gnu.uq.net.au)
Date: 09/01/04 

Date: 1 Sep 2004 04:58:14 GMT

D.McAnally@i'm_a_gnu.uq.net.au (David McAnally) writes:

>raf@tiki-lounge.com (Ross A. Finlayson) writes:

<snip>

>>Please name or describe a real element of
>>R^V[G] not in R^V, that is R, the set of all real numbers.

>Let the set F of forcing conditions be the set of all functions p whose
>domain is a finite subset of N and whose range is a subset of {0,1}, i.e.
>F = {p : p is a function, dom(p) is a finite subset of N, range(p) is a
>subset of {0,1}}. Define q <= p (q is stronger than p) if q extends p,
>i.e. p is a subset of q, i.e. dom(p) is a subset of dom(q) and p(n) = q(n)
>for all n in dom(p). It follows that p and q are compatible iff
>p(n) = q(n) for all n in the intersection of dom(p) and dom(q).

>Let G be a generic set in F (G is not necessarily an element of V).

>Let n be an element of N, and let D = {p in F : n in dom(p)}. If q is
>a forcing condition, and n is an element of dom(q), then q is stronger
>than q and q is an element of D.

>If q is a forcing condition and n is not an element of dom(q), let
>r = q u {(n,0)}, then r is a function, dom(r) is a finite subset of N
>and range(r) is a subset of {0,1}, and so r is a forcing condition,
>r is stronger than q, and n is an element of dom(r), and so r is an
>element of D.

>It follows that for all forcing conditions q, there exists a forcing
>condition r stronger than q such that r is an element of D. So D is
>dense. Since G is a generic set, then G intersects D. Let p be a common
>element of G and D, then n is an element of dom(p), and so n is an element
>of dom(UG) (where, for a set A, UA is the union of A).

>Since n is an arbitrary element of N, then dom(UG) = N.

>Since range(p) is a subset of {0,1} for all p in G, then range(UG) is a
>subset of {0,1}.

>Suppose UG is not a function, then there exists n in N such that (n,0) and
>(n,1) are both elements of UG. It follows that there exist p in G and
>q in G such that p(n) = 0 and q(n) = 1. Since n is an element of the
>intersection of dom(p) and dom(q), and p(n) and q(n) are not equal, then
>p and q are incompatible, contradicting the genericity of G. Since the
>assumption that UG is not a function leads to a contradiction, then UG is
>a function UG : N -> {0,1} in V[G].

>Let A = {n in N : (UG)(n) = 1}, then A is a subset of N in V[G].

>Let B be a subset of N in V, and define D = {p in F : exists n in dom(p)
>((n in B and p(n) = 0) or (n not in B and p(n) = 1))}. If q is a forcing
>condition and q is an element of D, then q is stronger than q and q is an
>element of D.

>Suppose q is a forcing condition and q is not an element of D, then
>for all n in dom(q) ((n in B and q(n) = 1) or (n not in B and q(n) = 0)).
>Since dom(q) is finite, then N-dom(q) is nonempty. Let m be an element
>of N-dom(q), and define r = q u {(m,0)} if m is an element of B, and
>r = q u {(m,1)} if m is not an element of B. Then r is a function,
>dom(r) is a finite subset of N, and range(r) is a subset of {0,1},
>so that r is a forcing condition, r is stronger than q, and ((m in B and
>r(m) = 0) or (m not in B and r(m) = 1)). It follows that r is an element
>of D.

>So D is a dense set. Since G is generic, then G intersects D, and so
>there exist p in G and n in dom(p) such that ((n in B and p(n) = 0) or
>(n not in B and p(n) = 1)). If n is an element of B, then p(n) = 0, so
>(UG)(n) = 0, so n is not an element of A. If n is not an element of B,
>then p(n) = 1, so (UG)(n) = 1, so n is an element of B. It follows that
>n is an element of either A or B, but not both, and so A and B are not
>equal. That is, for any subset B of N in V, there is a natural number n
>such that n is an element of the symmetric difference of A and B, and so
>A and B are not equal. It follows that A is not a subset of N in V, i.e.
>A is an element of V[G], but not an element of V.

>Let x = \sum_{n in N} 2^{-(UG)(n)}, then x is a real number in [0,2] in
>V[G], but x is not an element of V, i.e. x is a new real number.

That should have been x = \sum_{n in N} 2^{-n (UG)(n)}.

Note, by the way, that G is not an element of V.

David

-----

Loading