Re: Choice Question # 2

David C. Ullrich wrote:

> How about a formalization in ZF? First, if we take ZF
> plus notation (x,y) for ordered pairs, seems to me that
> AC is
>
> (S)((x)(x e S -> Ey y e x)
> -> Ef((x)(x e f -> Ea Eb(x = (a,b)))
> & (x)(x e S -> Ey Ez(z = (x,y) & z e f & y e x)
> & (w)(Ey(z = (x,w) & z e f) -> w = y)))

etc. etc.

>   (S)((x)(x e S -> Ey y e x)
>   -> Ef((x)(x e f -> Ea Eb((Ej ((a e x & j e x &
>   (i)(i e x -> (i = a or i = j))) & (a e j & b e j &
>   (i)(i e j -> (i = a or i = b)))))))
>   & (x)(x e S -> Ey Ez((Ej ((x e z & j e z &
>   (i)(i e z -> (i = x or i = j))) & (x e j & y e j &
>   (i)(i e j -> (i = x or i = y))))) & z e f & y e x)
>   & (w)(Ey((Ej ((x e z & j e z & (i)(i e z ->
>   (i = x or i = j))) & (x e j & w e j & (i)(i e j ->
>   (i = x or i = w))))) & z e f) -> w = y))))
>
> Seems simple enough...

In other words, my formalization is about 30 times simpler than yours.
Now, what does Occam's Razor say about this?

Don't you just love Occam's Razor?  It is the great Lie Detector.
When someone comes up with pages of unintelligible gobbledy gook and
then announces that after dozens of pages they have produced a certain
result - and boy are they proud of it - then you can just show a
simpler (authentic) derivation and by Occam's Razor his is absolute
junk.

That is definitely part of the mentality of the status quo.  If it's
complex it must be really advanced and a person would look foolish to
even question it.  But Occam's Razor reveals the stark reality!

( P(a) ^ SE(a,b) ) => SE(a,ch(a))

P is a set, SE is a relationship and ch is a function.  The above means
that the relation of P holding for a variable a and SE holding for
variables a and b, implies that SE holds for a and the result of
applying ch to a.  The Axiom of Choice is true iff there is a function
ch that satisfies this assertion.

Is there something unclear about this?

> ************************
> 
> David C. Ullrich

.

Relevant Pages

  • Re: Choice Question # 2
    ... David C. Ullrich wrote: ... what does Occam's Razor say about this? ... that the relation of P holding for a variable a and SE holding for ...
    (sci.logic)
  • Re: Choice Question # 2
    ... >David C. Ullrich wrote & Charlie-Boo wrote:> ... Except his was in a standard system, set theory, while your "formalization" was no formalization at all, unless we assume we're talking about a formal system that knows what you mean by a lot of the text and symbols you used. ... >> David C. Ullrich ...
    (sci.logic)
  • Re: Vector space or ots orthogonal
    ... Suppose that you have a vector subspace F in R^n. ... Could you explain please how this "dual" formalization was ontained, ... David C. Ullrich ...
    (sci.math)
  • Re: Finally...
    ... >I have always wanted an Astro 05 and a few more Razor 400's would be ... Better watch it, David. ... Someone "out there" might be packing a box up for ...
    (rec.models.rc.air)