11
$\begingroup$

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?

$\endgroup$
9
  • 8
    $\begingroup$ A proof can never be unique since we can prolong it with unnecessary steps. The shortest proof can however be unique. $\endgroup$
    – Peter
    Jul 18, 2023 at 20:15
  • 6
    $\begingroup$ Conceivably there could be two proofs of the same, minimal, length? $\endgroup$ Jul 18, 2023 at 20:20
  • 3
    $\begingroup$ Define "length." And define "distinct" as in proofs. And assuming you have $n$ proofs of a theorem, how do you ever prove there is not an $n+1$st proof left to be discovered? $\endgroup$ Jul 18, 2023 at 20:23
  • 3
    $\begingroup$ @Peter: "The shortest proof can however be unique." Explain... or better yet, prove. $\endgroup$ Jul 18, 2023 at 20:29
  • 4
    $\begingroup$ Any proof that contains more than a single axiom of your theory $T$, which would be most proofs, can be shuffled to change the order in which the axioms are introduced into the proof which shows that there are, at the very least, a large number of "minimal length proofs". As to what does it mean for two proofs to be "the same", well, wars started for less... $\endgroup$
    – Asaf Karagila
    Jul 18, 2023 at 20:35

2 Answers 2

18
$\begingroup$

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 ^_^

$\endgroup$
2
  • 1
    $\begingroup$ Oh, and on rereading your question, I notice you ask about theorems in ZFC. Let me briefly mention that your axioms (namely the axioms of ZFC) are distinct from your proof system, and it's the latter that is more relevant for your question. $\endgroup$ Jul 18, 2023 at 20:51
  • 1
    $\begingroup$ Thanks for such an interesting answer! I upvoted it and will let others answer too. $\endgroup$
    – Alex
    Jul 19, 2023 at 0:47
3
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .