Proving there is only one proof?

Question

I cannot seem to find or come up with an answer to the following question: In mathematics, is it possible to prove that there is only one (shortest) proof of a given theorem (say, in ZFC)?

Are there any (preferably natural) examples?

Answer 1

This depends strongly on both the proof system you're using and the theorem you're trying to prove. For this answer we'll work in a particularly simple proof system: Gentzen style natural deduction for propositional logic. If you aren't familiar with these kinds of formal derivations, I recommend looking into them! They're incredibly foundational for the kind of proof theory that you're asking about ^_^.

Now, in this system, there's a unique shortest proof that $A \land B \to A$, and here it is:

$$ \frac{\Large \frac{\overline{A,B \ \vdash \ A}}{A \land B \ \vdash \ A}}{\cdot \vdash A \land B \to A} $$

You can check that this is the unique shortest proof by just checking every derivation of length $\leq 3$, and seeing that this is the only one ending in $\cdot \vdash A \land B \to A$.

However, there are other theorems of this system which admit multiple shortest proofs. For instance, $A \land B \to A \lor B$. In this case we have both:

$$ \frac{\Large \frac{\LARGE \frac{\LARGE \overline{A, B \ \vdash \ A}}{A, B \ \vdash \ A \lor B}}{A \land B \ \vdash \ A \lor B}}{\cdot \vdash A \land B \to A \lor B} \quad \quad \quad \frac{\Large \frac{\LARGE \frac{\LARGE \overline{A, B \ \vdash \ B}}{A, B \ \vdash \ A \lor B}}{A \land B \ \vdash \ A \lor B}}{\cdot \vdash A \land B \to A \lor B} $$

Here the left side proof takes $A \land B$, deduces that $A$ is true, and thus that $A \lor B$ is true.

The right side proof takes $A \land B$, deduces that $B$ is true, and thus that $A \lor B$ is true.

You can see that these are genuinely distinct proofs (and indeed they have distinct computational content when you interpret these sequents as programs), but have the same length.

The subject of finding the shortest proofs for various classes of theorem in various proof systems is quite deep and rich, with many applications to computer science. See, for instance proof complexity.

---

I hope this helps ^_^

Answer 2

This was answered very well some time ago, but I don't see anywhere this direct, straightforward, and very different answer to the question you actually asked:

In mathematics, is it possible to prove that there is only one (shortest) proof of a given theorem ?

The answer is yes.

Since we're asking about a theorem, say $T$, there is by definition at least one proof of $T$, say one of length $n$. (“Length” here might mean “number of steps” or “number of symbols” or whatever you like; it doesn't matter.)

Now systematically generate all possible proofs of length up to $n$. Most of these will not be proofs of $T$; ignore these. At least one proof will be a proof of $T$, and among these proofs of $T$ there will be at least one of minimum length, say length $m$.

Either there are multiple proofs of $T$ of length $m$, or only one. Either way, we have the answer to the question of whether the minimum-length proof of $T$ is unique, and a proof of that answer.

It's a really long proof! But it is watertight.