This discussion continues from the introductions of an alternative definition of one-to-one correspondence THERE.

We have given three "definitions" of sorts to the concept of one-to-one correspondence between two classes, symbolized as A ~~ B.

We gave a suggestive description of the concept informally, then gave a different equivalent description interms of the existence of inverse functions, then a third explanation was in terms of the existence of bijections. In order make reasoning about A ~~ B possible in the existing system, we must somehow extend the system with new "axioms" about this relation. We could add some new primitive axioms that declare the existence of this new relation and some basic facts about it. But as usual, we have elected to find an existing combination of concepts that we can informally understand to be equivalent to the A ~~ B relation.

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

Def  A ~~ B == f:(AB), g:(BA). InvFuns(A; B; f; g)

As the principle definition and prove

Thm*  (f:(AB). Bij(A; B; f))  (A ~ B)

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 A ~~ B, but the "content" of the proof is essentially that existence of a bijection is equivalent to the existence of inverse functions.

If you trace down the definitions of Bij(A; B; f) and A ~~ B, you will see that they share almost nothing, so we are relating significantly different concepts here. Click HERE for definition comparison.

Examination of the proof will reveal that it reduces to two lemmas expression the opposite directions of implication, 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 it's a bijection. The second uses the inverse of a function to show its a bijection.

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