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: 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> <40b7c771-1b7d-4076-96ff-384682c77b2bn@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 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) 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() :=3D X and codom() =3D Y.)=20 > >=20 > > Again, if f =3D and g =3D , 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( e gra & e gr= a -> y =3D z) such that {x : Ey( e gra)} =3D X and {y : Ex( e g= ra)} c Y. Actually, AfAXAY(f: X --> Y <-> Eg(f =3D & g c X x Y & {x e UUg : Ey(= e g)} =3D X)) ....might be used as an axiom or definition.