Re: Replacement of Cardinality

Am 26.08.2024 um 00:04 schrieb Moebius:

Am 24.08.2024 um 06:30 schrieb Jim Burns:

Seems you really don't get it. (*sigh*)
 Without proof of
           1. Ex(raimex(x))
and
          2. AxAy(raimex(x) & raimex(y) -> x = y)
 we may not use the "definition"
           x = the_raimex :<-> rational(x) & imaginative(x) & experiencing(x) & a_being(x)
 In other words, we are not allowed to talk about _the_ raimex (not having a proof that there is exactly one such entity, i.e. exactly one x such that x is a raimex).

If we would, say, allow for the "definition"
            x = 1/0 :<-> 0 * x = 1
and hence the "lemma"
            ~Ex(x = 1/0) ,
we would get:
            Ax(x =/= 1/0) .
Then by specification (AE) we would get:
            1/0 =/= 1/0
from this, and then by (EI):
            Ex(x =/= x) .
Not a desirable result.
(That's why _one_ of the rules for proper definitions of constants requires an existence proof first.)