Re: Replacement of Cardinality

Am 26.08.2024 um 16:08 schrieb Moebius:

Again, that's why we have to prove an existence claim
            Ex(Px)
 before stating/using the defintion
            x = c :<-> Px .
 Actually, in addition to this proof we also need a proof of "uniquines" before ...

Here's an argument for the claim that we need that proof of "uniquines" too.
Def. (JB style):   x = c :<-> x e {0, 1}.
Well, clearly there is an x such that x e {0, 1}. So, such an x exists. Great.
Now, clearly
            0 e {0, 1}
and hence from our "definition":
            0 = c       (1) .
And clearly
            1 e {0, 1}
and hence from our "definition":
            1 = c       (2) .
But from (1) and (2) we get:
            0 = 1 .
Not a desirable result.
_____________________________________________________________________________
Do avoid this undesirable results there's the requirement to prove
            ExPx
and
            AxAy(Px & Py -> x = y)
before stating the definition
            x = c :<-> Px ,
where /c/ is a term not already part of the system (as a primitive term or a term introduced by an earlier definition).