X-Received: by 2002:ac8:4e51:0:b0:31b:efe0:aa24 with SMTP id e17-20020ac84e51000000b0031befe0aa24mr16483349qtw.635.1656767499262;
        Sat, 02 Jul 2022 06:11:39 -0700 (PDT)
X-Received: by 2002:a05:6870:f143:b0:f3:3d31:1da9 with SMTP id
 l3-20020a056870f14300b000f33d311da9mr12909080oac.134.1656767498998; Sat, 02
 Jul 2022 06:11:38 -0700 (PDT)
Path: ...!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.logic
Date: Sat, 2 Jul 2022 06:11:38 -0700 (PDT)
In-Reply-To: <ffa6bc1c-101a-4631-8a7c-6ef47f18ebb3n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=163.182.226.42; posting-account=OWfgwwgAAADQpH2XgMDMe2wuQ7OFPXlE
NNTP-Posting-Host: 163.182.226.42
References: <1b8e09f0-914a-4324-9c56-048308925691n@googlegroups.com>
 <a6fbd950-755d-4708-8f45-0a14e37af8c6n@googlegroups.com> <1e23164b-4207-4a48-8553-b8cdc0b522f8n@googlegroups.com>
 <ba3c9e00-d62b-46b0-b172-a5aabe67e6d1n@googlegroups.com> <ffa6bc1c-101a-4631-8a7c-6ef47f18ebb3n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <115568ca-08ce-45ae-bb08-2f69dd986493n@googlegroups.com>
Subject: Re: Bijectivity is Transitive, Formal Proof
From: Dan Christensen <Dan_Christensen@sympatico.ca>
Injection-Date: Sat, 02 Jul 2022 13:11:39 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Bytes: 3529
Lines: 46

On Saturday, July 2, 2022 at 5:22:37 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Freitag, 1. Juli 2022 um 19:03:16 UTC+2:=20
> > On Friday, July 1, 2022 at 5:05:00 AM UTC-4, Mostowski Collapse (Jan Bu=
rse) wrote:=20
> > > Since this equality here, is an existential type:=20
> > > u ~ v :<=3D> EXIST(f):[ f : u -> v, f bijective]=20
> > > It anyway begs the question why you use your=20
> > > nonsense function axiom.=20
> > Jan Burse is pissed off that my standard definition (line 29) does not =
include his "dark" elements =C3=A0 la Muckenheim (WM). He wants to make log=
ical inferences about functions outside of their domains of definition. Usu=
ally they are simply said to be undefined outside of their domains. Jan Bur=
se still doesn't get it.=20
> >=20
> > [snip]=20
> > > Would get much shorter without the detour=20
> > > over your function axiom nonsense.=20
> > Not really. Have you never had to prove the existence of a function? Th=
e function axiom establishes the standard requirements for the graph set of=
 any function. That would be unavoidable even in your wonky system, Jan Bur=
se.=20
> >=20
> You can shorten your proofs considerably, when you don't=20
> use your function axiom. The definition of ~ which was=20
>=20
> at the center of much investigation by Cantor and others=20
> 100 years ago doesn't need any function axiom. You just=20
>=20
> define it as follows:
> u ~ v :<=3D> EXIST(f): [ f : u -> v , f bijective ]

Now, you need to formally define "f: u -> v" and "bijective".=20

> Where f is a set-like functions aka a graph.  You can directly=20
> use graphs...

Very awkward for most applications and prone to some wonky results, e.g. yo=
ur "dark" elements. Better and much more convenient to have: ALL(a):ALL(b):=
[a in dom & b in cod =3D> [f(a)=3Db <=3D> (a, b) in graph]]. Then f(x) is u=
ndefined/unspecified for x not in dom.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com