# Do there exist true statements with only one proof? [closed]

The Pythagorean Theorem, for instance, has many, many proofs which are fundamentally different and use what appear to be very different ideas. These range from static geometric constructions to similarity factor arguments.

My question is: are there any provable statements which do not have more than one way to prove them (up to proofs being "effectively the same" in some way)? If so, what is this notion of "the same", and how do we know there is only one way to prove something, or that no such provable statements exist?

Equivalently, can everything which is provable be proved in more than one way? We know some true statements cannot be proven at all by Godel, but do some have just one proof? (or finitely many?)

EDIT: The notion of "effectively the same" and what that means is designed to be a part of the question; asking whether such a notion formally exists and, if so, what that notion is.

Derik Elkins does a very good job of answering with similar level of detail to what was asked. The answer was that, yes, there are some statements which only have one "normal form", and thus all their proofs are equivalent.

## closed as unclear what you're asking by Paul Frost, Parcly Taxel, Leucippus, Don Thousand, GNUSupporter 8964民主女神 地下教會Oct 16 '18 at 6:13

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

One particular form of the Curry-Howard correspondence links terms in typed lambda calculi to proofs in various logics. The archetypal example being the simply typed lambda calculus and intuitionistic propositional logic. From this perspective, your question is equivalent (using the same notion of "effectively the same" as the previous paragraph) to asking if there are types that have only one normal form inhabitant. The answer to this is definitely "yes" though it can depend on which logic you're using and some other details. A widely used example is the type $$\forall A.A\to A$$ in the polymorphic lambda calculus has only one (normal form) inhabitant, namely the polymorphic identity function (formally: $$\Lambda\tau.\lambda x\!:\!\tau.x$$). The polymorphic lambda calculus corresponds to intuitionistic second-order propositional (not predicate) logic. For contrast, $$\forall A.A\to(A\to A)$$ has two distinct normal form proofs corresponding to the terms $$\Lambda\tau.\lambda x\!:\!\tau.\lambda y\!:\!\tau.x$$ and $$\Lambda\tau.\lambda x\!:\!\tau.\lambda y\!:\!\tau.y$$.