Re: Replacement of Cardinality

Am 26.08.2024 um 03:05 schrieb Moebius:

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.

Especially not in a context where we have the axiom or theorem
               Ax(x = x) .

(That's why _one_ of the rules for proper definitions of constants requires an existence proof first.)