AX-E\AGENDA.TXT           

1997 August 14

Ideas for theorems:

AxCh -> equal(fix(composite(CHOICE,SINGLETON)),V).
AxCh -> equal(composite(CHOICE,SINGLETON),Id).                   % AC-SG-2

Comments.

The first equation follows from the following calculation:

   fix(CHOICE o SINGLETON) \subclass fix(E~ o SINGLETON) = fix(Id) = V

If fix(x) = V, then Id \subclass x, so the following corollary holds:

        Id \subclass CHOICE o SINGLETON 

The equation CHOICE o SINGLETON = Id now follows from the observation
that
       CHOICE o SINGLETON \subclass E~ o SINGLETON = Id.

I was unable to prove this in Otter, but I did not try very hard.


2000 March 2

Here is a theorem that looks innocent enough, but may require the
axiom of choice:


image(IMAGE(FIRST),P(x)) = P(D(x)).

Using the GOEDEL program one can show it holds when  x  is a
set:  When  x  is a set, and y is a subset of D(x), the
restriction  composite(x,id(y))  is a set, and its domain
is  y.

If  x  is not a set, then there is no guarantee that the
restriction of x to y will be a set, but one might be able
to use the axiom of choice to find a function contained in
that restriction.

2000 June 4

If f is a function, then g = composite(CHOICE,VERTSECT(inverse(f)))
is another function which choses for each value v in R(f) some
argument u in D(f) with v = apply(f,u).  If we restrict  f  to
R(g), we should get a one-to-one function with the same range as f.
Thus we should be able to prove that if f is any small function, there
is a subset of D(f) that is equipollent to R(f):

AxCh -> (all x (member(x,FUNS) -> 
                member(pair(D(x),R(x)),composite(Q,inverse(S))))).

Hence:

AxCh -> (all x (FUNCTION(x) -> subclass(IMAGE(x),composite(Q,inverse(S))))).