Some other answers have alluded to this, but just to spell it out explicitly: The <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence#Curry.E2.80.93Howard.E2.80.93Lambek_correspondence">Curry-Howard isomorphism</a>, in one of its simpler forms, says that objects of the free cartesian closed category CCC[S] on a set S of objects correspond to statements of the multiplicative fragment of intuitionistic logic (things we can build from /\ and &rArr;) with free variables from S, and there is at least one morphism P &rarr; Q in CCC[S] iff P &rArr; Q is a theorem.  Thus we can regard a morphism P &rarr; Q as a "proof" of P &rArr; Q.  There may be several morphisms from P to Q; for instance if A ∈ S and P = A &times; A, Q = A, then there are exactly two morphisms from P to Q (projection to the first or second factor), which we can regard as two different proofs of the theorem (A /\ A) &rArr; A.

Probably the easiest way to see what the different proofs are in this system is to use the third part of the Curry-Howard isomorphism: morphisms P &rarr; Q in CCC[S] correspond to functions in the simply typed lambda calculus of type P &rArr; Q, where &times; in CCC[S] is interpreted as the product of types and the internal Hom as a function type.  For instance there are two functions of type (A * A) &rarr; A, namely &lambda;(a, b). a and &lambda;(a, b). b.  A more interesting example: the theorem (A &rArr; A) &rArr; (A &rArr; A) has one proof for every natural number, corresponding to &lambda; f. &lambda; x. f (f (... (f x)...)).  See <a href="http://math.ucr.edu/home/baez/week240.html">This Weeks' Finds week 240</a> for more along these lines.