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 ⇒) with free variables from S, and there is at least one morphism P → Q in CCC[S] iff P ⇒ Q is a theorem. Thus we can regard a morphism P → Q as a "proof" of P ⇒ Q. There may be several morphisms from P to Q; for instance if A ∈ S and P = A × 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) ⇒ 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 → Q in CCC[S] correspond to functions in the simply typed lambda calculus of type P ⇒ Q, where × 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) → A, namely λ(a, b). a and λ(a, b). b. A more interesting example: the theorem (A ⇒ A) ⇒ (A ⇒ A) has one proof for every natural number, corresponding to λ f. λ 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.