Proof that Counting is Unique

Thm*  (A ~ m)  (A ~ k)  m = k

See Introduction to Counting.

We shall build this argument from a lemma about injections on standard finite types,

Thm*  (f:(mk). Inj(m; k; f))  mk,

and exploiting the connection between X ~ Y and injections, and the connection between xy and equality.

Assume a class has size m, but also has size k;
show m must actually be k.
Each direction of the equality, namely,

mk and km,

may be proved in the same way, so we generalize the goal slightly to

x,y:. (x ~ y)  xy.

Once this is proved, mk and km follow easily from it since m ~ k and k ~ m follow easily from our assumptions and the fact that X ~ Y is an equivalence relation, i.e.,

Thm*  EquivRel X,Y:Type. X ~ Y.

So, it is enough to show that xy, assuming that x ~ y.
The connection between X ~ Y and bijection is established by

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

And since being an injection is part of being a bijection, i.e.,

Def  Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f),

xy follows from the lemma

Thm*  (f:(mk). Inj(m; k; f))  mk.

QED

A corrolary is Thm*  a,b:. (a ~ b)  a = b.

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