5
$\begingroup$

This question is somehow based on my belief that every theorem has a short and simple proof. By "proof" I mean:

  • Proving an statement
  • Disproving a statement
  • Proving that a statement is undecidable

Once we have formalized what we understand for a "step" in a proof, could it be proven that every theorem has a proof consisting of less than $n$ steps? If so:

  • What would be the (minimal) value of $n$?
  • Such a proof would be about all proofs so what would it say about itself?
  • Could there be (in some sense) proofs with a non-integer number of steps?
$\endgroup$
12
  • 5
    $\begingroup$ You could try to build each theorem up by forming it out of small lemmas that you then call theorems. For instance, the proof of Fermat's last theorem might be summarized by "A exists, which contradictions theorem 3.4.3. Q.E.D." $\endgroup$
    – user357980
    Commented Sep 6, 2016 at 13:31
  • 3
    $\begingroup$ en.wikipedia.org/wiki/Proof_complexity ? $\endgroup$
    – Clement C.
    Commented Sep 6, 2016 at 13:37
  • 3
    $\begingroup$ Depends how one would define a "step", but if our definition somehow only allows steps to have somehow bounded "complexity" (i.e. doing 100 things in one step wouldn't be allowed), then there would be only a finite number of possible steps, so there would be only finitely many theorems to be proven in $n$ steps. But we can make up infinitely many theorems... $\endgroup$
    – Wojowu
    Commented Sep 6, 2016 at 13:38
  • 1
    $\begingroup$ There are not uncountably many theorems in most axiomatic systems. @TravisJ $\endgroup$
    – Thomas Andrews
    Commented Sep 6, 2016 at 13:58
  • 2
    $\begingroup$ Why do you believe that every theorem has a short and simple proof? $\endgroup$
    – David K
    Commented Sep 6, 2016 at 18:16

3 Answers 3

Reset to default
4
$\begingroup$

Let $f(n)$ be any computable (total) function. Then there must be a theorem $T$ of length $N$ such that the shortest proof of $T$ is longer than $f(N)$ steps.

This is because, if such a $T$ did not exist, we could solve known unsolvable questions.

This result assumes the following basic fact about the "length" of proofs:

  1. Given any $m$, there are only finitely many proofs of length at most $m$.
  2. There exists a program which can take $m$ as input an return the list of proofs of length $m$.
$\endgroup$
3
  • 1
    $\begingroup$ In particular, the question "Is there a formal proof (with no extra axioms) of formula $\phi$?" cannot be solved by any algorithm; this is the so-called undecidability of logical validity in first-order logic. If there was a bound on the length of the shortest formal proof, computable from $\phi$, then the question could be answered by brute-force search. $\endgroup$
    – Carl Mummert
    Commented Sep 6, 2016 at 19:53
  • $\begingroup$ Yeah, that was the example I was thinking of, but I could not quite remember if it was correct. @CarlMummert But I knew, at least, it would allow a solution to solve the halting problem. I decided against stating that example explicitly because (1) I vaguely knew there was a better example, and (2) it is jumping more deeply into computability than the intuitive notion of "computable function." $\endgroup$
    – Thomas Andrews
    Commented Sep 6, 2016 at 20:02
  • 1
    $\begingroup$ Nice answer, but I think you need to work a bit harder to get a convincing argument if length means the number of steps in the proof. In most logical systems there are infinitely many proofs of a given length, because a short proof can involve arbitrarily large formulas. So (for most logical systems) your argument works if you measure the size of a proof tree by the number of symbols it contains, but not if you measure it by the number of inference steps. $\endgroup$
    – Rob Arthan
    Commented Sep 6, 2016 at 22:30
2
$\begingroup$

There are infinitely many theorems, if by "theorem" we just mean "true mathematical statement". If we allow $k$ distinct kinds of step, there are only $k^n$ different proofs of length $n$ (and many of them would prove the same things over and over). So no, there's no $n$ so that every theorem can be proven in $n$ steps.

As a matter of fact, Godel's Incompleteness Theorem states that there is some true mathematical statement - "theorem" by the definition I suggested earlier - which has no proof at all, given a definition of a "step" in a proof.

On the other hand, just playing with this idea, we could say a "theorem" is a true mathematical statement for which a proof has been written down. Then there is indeed a $n$ so that every theorem has a proof of length at most $n$ - take $n$ to be the number of steps required to write the longest proof that has ever been written (probably the classification theorem for finite simple groups, but I'm not sure). But I don't think there's anything interesting to say about $n$, apart from that it's HUGE as long as your proof system is reasonably simple.

$\endgroup$
0
$\begingroup$

surely a theorem doesn't need to conform to any real quality requirements, so it could contain an huge number of steps that need to be proved, greater than any n you think of.

$\endgroup$

You must log in to answer this question.

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