X-Received: by 2002:a05:622a:6115:b0:2f1:d8fa:84aa with SMTP id hg21-20020a05622a611500b002f1d8fa84aamr12062858qtb.689.1650890366648;
        Mon, 25 Apr 2022 05:39:26 -0700 (PDT)
X-Received: by 2002:a05:6870:f146:b0:db:c90:99bb with SMTP id
 l6-20020a056870f14600b000db0c9099bbmr6721231oac.55.1650890366395; Mon, 25 Apr
 2022 05:39:26 -0700 (PDT)
Path: ...!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.logic
Date: Mon, 25 Apr 2022 05:39:26 -0700 (PDT)
In-Reply-To: <ea3b1065-19da-4d72-b567-97da2f001bc6n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=79.206.195.177; posting-account=-75WZwoAAABL0f0-07Kn6tvNHWg7W9AE
NNTP-Posting-Host: 79.206.195.177
References: <5247dac7-7489-4b9f-a6c4-8da8ee50c22en@googlegroups.com>
 <651d491d-f67e-4930-9135-9f68764c91c1n@googlegroups.com> <d019f35f-407a-4297-8800-2099eaecbddcn@googlegroups.com>
 <40b7c771-1b7d-4076-96ff-384682c77b2bn@googlegroups.com> <ea3b1065-19da-4d72-b567-97da2f001bc6n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <8ee09a9d-df7e-46cd-896d-eb0d38c116een@googlegroups.com>
Subject: Re: How to formally construct a function in DC Proof
From: Fritz Feldhase <franz.fritschee.ff@gmail.com>
Injection-Date: Mon, 25 Apr 2022 12:39:26 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Bytes: 3667
Lines: 51

On Monday, April 25, 2022 at 2:29:03 PM UTC+2, Fritz Feldhase wrote:
> On Monday, April 25, 2022 at 1:19:17 PM UTC+2, Fritz Feldhase wrote:=20
> > On Monday, April 25, 2022 at 6:14:40 AM UTC+2, Dan Christensen wrote:=
=20
> > > On Sunday, April 24, 2022 at 4:04:15 PM UTC-4, Fritz Feldhase wrote:=
=20
> > > > >=20
> > > > > =3D> ALL(a):[a in x =3D> id'(a)=3Did(a)]]]]=20
> > > > >=20
> > > > Right. But this does n o t prove id' =3D id.=20
> > > >=20
> > > Recall that an axiom of functional equality is not built into the cur=
rent version of DC Proof.=20
> > Since your current approach concerning functions has some proplems.=20
> > > You might say that id and id' are "equivalent" functions ON THE DOMAI=
N x.=20
> > Rather they just "agree" an x.=20
> >=20
> > x might not even be a subset of dom(id) and dom(id').=20
> >=20
> > It seems to me that you still don't get it. Ax(x e X -> f(x) e Y) does =
not ensure that X is the domain and Y is the codomain of f. There's a reaso=
n why we use the expression "f: X --> Y" (which SAYs that "f is a function =
from X in Y") in math. You would have to "model" this expression in DC Proo=
f. Actually, to represent it as a tripple (just like Bourbaki did) <gra, X,=
 Y> might be a god idea.
> _good_ idea. :-)
> > In this case f =3D g iff f_1 =3D g_1 & f_2 =3D g_2 & f_3 =3D g_3 just f=
rom extensionality.=20
> >=20
> > Hence f =3D g iff dom(f) =3D dom(g) & codom(f) =3D codom(g) & Ax(x e do=
m(f) -> f(x) =3D g(x))=20
> >=20
> > (with dom(<gra, X, Y>) :=3D X and codom(<gra, X, Y>) =3D Y.)=20
> >=20
> > Again, if f =3D <gra, X, Y> and g =3D <gra', X', Y'>, then from extensi=
onality=20
> >
> > f =3D g iff X =3D X' & Y =3D Y' & gra =3D gra'.
> >=20
> > Two functions f, g are identical iff they have the same domain, the sam=
e codomain and the same graph. Simple as that.
> gra must be a set of ordered pairs with AxAyAz(<x, y> e gra & <x, z> e gr=
a -> y =3D z) such that {x : Ey(<x, y> e gra)} =3D X and {y : Ex(<x, y> e g=
ra)} c Y.

Actually,

AfAXAY(f: X --> Y <-> Eg(f =3D <g, X, Y> & g c X x Y & {x e UUg : Ey(<x, y>=
 e g)} =3D X))

....might be used as an axiom or definition.