Path: ...!feeds.phibee-telecom.net!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Moebius <invalid@example.invalid>
Newsgroups: sci.math
Subject: Re: Replacement of Cardinality
Date: Mon, 26 Aug 2024 03:05:50 +0200
Organization: A noiseless patient Spider
Lines: 47
Message-ID: <vagkdf$24vpo$6@dont-email.me>
References: <hsRF8g6ZiIZRPFaWbZaL2jR1IiU@jntp> <va31ko$3havl$1@dont-email.me>
 <VqqLFKi62z9rl82Gg4Mxsdp4YYg@jntp> <va4h96$3r7nv$1@dont-email.me>
 <H5iV5HXUBwUzWtVKRZj7h4N2LdA@jntp>
 <ff390a80279179f6d2f4660ed19c150a88c787d6@i2pn2.org>
 <va4rcm$3soiv$1@dont-email.me> <maptLlB5uFyelg509mbdgWw1yGc@jntp>
 <980a0ec7476c9dc5823e59b2969398bd39d9b91d@i2pn2.org>
 <va5c09$3vapv$1@dont-email.me> <h6Deptvp2nWZ7A-WxxE_8LCEIYY@jntp>
 <8d5b0145-b30d-44d2-b4ff-b01976f7ca66@att.net> <vab841$13f3u$1@dont-email.me>
 <c47457bf-c2bf-4ba8-8f5b-879c59a9b464@att.net> <vag9q0$23e8p$2@dont-email.me>
Reply-To: invalid@example.invalid
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 26 Aug 2024 03:05:52 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="4b1539e64c5d00758bb452bc01f8a2b3";
	logging-data="2260792"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19kQmajAApuTMf9lzbLRX2/"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:Zaej3aiRxU94+5+5rWlJg1Biysw=
Content-Language: de-DE
In-Reply-To: <vag9q0$23e8p$2@dont-email.me>
Bytes: 2637

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.)