41
$\begingroup$

Hilbert's 23 problems, ten of which were presented at the 1900 ICM in Paris, are too famous for any mathematician to not know. If one reads the descriptions of the problems in Hilbert's paper, one realizes that some questions are concrete whereas the others are stated somewhat vaguely. The 24th problem that I will quote below definitely falls into the latter category.

It seems that there was a 24th problem which was "cancelled". The following is from an article that appeared in American Mathematical Monthly in 2003.

Let me begin by presenting the problem itself. The twenty-fourth problem belongs to the realm of foundations of mathematics. In a nutshell, it asks for the simplest proof of any theorem. In his mathematical notebooks [38:3, pp. 25-26], Hilbert formulated it as follows (author's translation):

The 24th problem in my Paris lecture was to be: Criteria of simplicity, or proof of the greatest simplicity of certain proofs. Develop a theory of the method of proof in mathematics in general. Under a given set of conditions there can be but one simplest proof. Quite generally, if there are two proofs for a theorem, you must keep going until you have derived each from the other, or until it becomes quite evident what variant conditions (and aids) have been used in the two proofs. Given two routes, it is not right to take either of these two or to look for a third; it is necessary to investigate the area lying between the two routes. Attempts at judging the simplicity of a proof are in my examination of syzygies and syzygies [Hilbert misspelled the word syzygies] between syzygies [see Hilbert [42, lectures XXXII-XXXIX]]. The use or the knowledge of a syzygy simplifies in an essential way a proof that a certain identity is true. Because any process of addition [is] an application of the commutative law of addition etc. [and because] this always corresponds to geometric theorems or logical conclusions, one can count these [processes], and, for instance, in proving certain theorems of elementary geometry (the Pythagoras theorem, [theorems] on remarkable points of triangles), one can very well decide which of the proofs is the simplest. [Author's note: Part of the last sentence is not only barely legible in Hilbert's notebook but also grammatically incorrect. Corrections and insertions that Hilbert made in this entry show that he wrote down the problem in haste.]

The paper I linked above discusses the history and the role of Hilbert's problems and I think is worth reading. Most of mathematical logic, as we know it right now, did not exist when this question was asked and you can simply disregard the question by saying "this is not a mathematical question". On the other hand, the same could be said about the second problem on the consistency of arithmetic today, if mathematicians did not develop the necessary tools to deal with this problem.

My point is that one might be able to answer Hilbert's 24th problem if one finds the "correct" statement of the problem. With our current knowledge and understanding of mathematical logic, can we define a criteria for a proof to be "simple"? Have there been any attempts to define such a notion? Should "simple" merely mean "short"?

In Thiele's article, you can find some quotations in Section 5 but they do not really give any useful information about how Hilbert perceived the word "simple". Having stumbled upon this article only today, I admit that I have not searched for other articles yet. So I would also appreciate being directed to other books and articles on this cancelled 24th problem.

$\endgroup$
  • 2
    $\begingroup$ Does syzygy have a formal meaning in mathematical logic? Is the idea to make an analogy of the Hilbert syzygy theorem about some sort of free resolutions of proofs or sets of axioms? $\endgroup$ – Douglas Zare Oct 15 '15 at 4:45
  • $\begingroup$ @DouglasZare: I think the syzygy's he refers to are the ones used in algebra. Thiele speculates about what Hilbert could have meant in Section 11. Personally I'd rather not speculate without having a good grasp on why he used that analogy. $\endgroup$ – Burak Oct 15 '15 at 4:56
  • 7
    $\begingroup$ "Quite generally, if there are two proofs for a theorem, you must keep going until you have derived each from the other, or until it becomes quite evident what variant conditions (and aids) have been used in the two proofs." Arguably, reverse mathematics falls into this scheme. I say "arguably" because reverse mathematics is concerned only with the axioms used in a proof, not the length or other structure of the proof, so the whole text suggests this isn't what he meant (hence my comment rather than an answer). Still, it's interesting to note. $\endgroup$ – Noah Schweber Oct 15 '15 at 7:15
  • 1
    $\begingroup$ I think "proof relevance" is a pertinent phrase... $\endgroup$ – David Roberts Oct 15 '15 at 9:59
  • 1
    $\begingroup$ My guess is either "too broad" or "opinion-based", considering the fact that the question asks what the definition should be, which is subjective. It seems that you can, for example, discuss Turing machines on MO but you cannot discuss the Church-Turing thesis. $\endgroup$ – Burak Oct 17 '15 at 20:30
32
$\begingroup$

some recent contributions to Hilbert's 24th problem:


the earliest work on Hilbert's 24th problem is by Gerhard Gentzen (1933); it was discussed in Logic's Lost Genius: The Life of Gerhard Gentzen, by E. Menzler-Trott:

Gentzen's doctoral thesis "Investigations into logical reasoning" from 1933 was lost, and only rediscovered recently. (The main results were reinvented by D. Prawitz in the 1960's.) An English translation from 2008 can be found here: Gentzen's Proof of Normalization for Natural Deduction.

$\endgroup$
  • 2
    $\begingroup$ Upvoted brasillian times for good scholarship. $\endgroup$ – paul garrett Oct 15 '15 at 23:10
19
$\begingroup$

As Carlo Beenakker's references indicate, we are still a long way off from having a satisfactory definition of the "simplicity" of a proof. There are some technical definitions of simplicity that can serve as helpful heuristics for automatic theorem provers, but they do not capture most aspects of our intuition for what "simplicity" means.

The June 2015 issue of Philosophia Mathematica was devoted to the question of mathematical "depth." Depth is arguably related to simplicity; a deep theorem could perhaps be defined as a simple theorem that has no simple proof. Again if one reads the papers in this volume, the general message seems to be that we are a long way from having a satisfactory account of the concept of depth.

Incidentally, my personal suspicion is that if a satisfactory theory of simplicity is developed, the "normal" state of affairs will be that a theorem does not have a unique simplest proof. The quest for a definition of simplicity that makes every theorem have a unique simplest proof strikes me as similar to the quest for a consistency proof for mathematics or the quest for a decision procedure for Diophantine equations: A childhood dream that we must eventually learn to let go of.

$\endgroup$
  • 2
    $\begingroup$ It might indeed be that this quest is a childhood dream and cannot be achieved. Nevertheless, I do not think that we should abandon it, considering how much we learned from other unattainable quests like consistency of mathematics or decision procedure for Diophantine equations. $\endgroup$ – Burak Oct 16 '15 at 16:27
  • 1
    $\begingroup$ "unique simplest proof" - using propositions as types and an Id-types, one could quite naturally have proofs of facts that are not equal, using Id, and otherwise incomparable by the 'directed' notion of 'simpler' $\endgroup$ – David Roberts Oct 17 '15 at 1:01
11
$\begingroup$

Homotopy type theory addresses a related issue (although without particularly saying anything about simplicity). The statement x: A, usually read as "x is of type A" can also be read as "x is a proof of the proposition A". Now, if we think of types as homotopy types, this encourages us to think about the topology of the space of proofs of A. For example, as Hilbert suggests, we may look for a path between two proofs, (equivalently read as an instance in the equality type Eq[A]).

The canonical example of this is the Eckmann-Hilton argument showing that $\pi_2(X)$ is abelian, where there are two essentially different proofs, determined by which way we rotate $\alpha$ and $\beta$ around each other in the following sequence of diagrams:

An illustration of the Eckmann-Hilton argument

(Thanks to John Baez, from whom I stole this diagram.)

On the other hand, the corresponding two proofs that $\pi_3(X)$ is abelian are themselves connected by a path.

$\endgroup$
8
$\begingroup$

"Simplest" seems hard to quantify but there is a body of technical work on the concept of "proof identity" (determining if two proofs are essentially the same) which seems related. This covers some history at the beginning:

Added: Older MO thread about proof identity:

$\endgroup$
4
$\begingroup$

Since this question has been bumped to the first page, it seems safe to mention a paper that I wrote in 2002, developing a notion of simplicity in first-order logic and a better-behaved one in propositional logic (so in a much more restricted context than what Hilbert had in mind). The MathSciNet data are

MR2023260 (2004j:03014) Reviewed Blass, Andreas(1-MI) Resource consciousness in classical logic. (English summary) Games, logic, and constructive sets (Stanford, CA, 2000), 61–74, CSLI Lecture Notes, 161, CSLI Publ., Stanford, CA, 2003.

A pre-publication version is available at http://www.math.lsa.umich.edu/~ablass/llc9.pdf .

$\endgroup$
0
$\begingroup$

Slightly tangentally, one might also look at the contribution of Gödel, as well: "Über die Länge von Beweisen", reprinted with English translation in his Collected Works, volume 1.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.