One-to-One Correspondence: equivalence of two characterizations.

We have given three "definitions", of sorts, to the concept of one-to-one correspondence between two classes, denoted by (f is 1-1 corr).

We gave a suggestive description of the concept informally, then gave a different, purportedly equivalent, description in terms of the existence of inverse functions, then a third explanation was bijection. In order make formal reasoning about (f is 1-1 corr) possible we must somehow add new "axioms" about this predicate. We could add some new primitive axioms that declare the existence of this new predicate and some basic facts about it. But as usual, we have elected to find a combination of concepts that we can informally understand to be equivalent to one-to-one correspondence, and that we can already formally reason about.

When there are several candidates for defining a new symbol, it is typical to pick one as the principal definition, and demonstrate the equivalence of the others. In our case, we chose to use

Def  f is 1-1 corr == g:(BA). InvFuns(A;B;f;g)

as the principal definition, and prove

Thm*  Bij(A; B; f)  f is 1-1 corr

as a theorem, although we could just as easily have chosen the reverse. The use of this theorem will be pretty much as if it were a definition of (f is 1-1 corr), but the "content" of the proof is essentially that being a bijection is equivalent to having an inverse.

Examination of the proof will reveal that it reduces to two lemmas expressing the opposite directions of the equivalence, namely,

Thm*  f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A;B;f;g))

Thm*  InvFuns(A;B;f;g)  Bij(A; B; f)

The proof of the first theorem shows how to construct an inverse of a function given that it's a bijection. The second uses the inverse of a function to show that it is a bijection.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html