School of Mathematical and Natural Sciences , Arizona State University , West Campus, PO Box 37100, Phoenix, AZ 85069-7100 , USA.
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180035. doi: 10.1098/rsta.2018.0035.
By looking at concrete examples from elementary geometry, we analyse the manner in which the simplicity of proofs could be defined. We first find that, when presented with two proofs coming from mutually incompatible sets of assumptions, the decision regarding which one is simplest can be made, if at all, only on the basis of reasoning outside of the formal aspects of the axiom systems involved. We then show that, if the axiom system is fixed, a measure of proof simplicity can be defined based on the number of uses of axioms deemed to be deep or valuable, and prove a number of new results regarding the need to use at least three times some axioms in the proof of others. One such major example is Pappus implies Desargues, which is shown to require three uses of Pappus. A similar situation is encountered with Veblen's proof that the outer form of the Pasch axiom implies the inner form thereof. The outer form needs to be used at least three times in any such proof. We also mention the likely conflicting requirements of directness of a proof and the length of a proof. This article is part of the theme issue 'The notion of 'simple proof' - Hilbert's 24th problem'.
通过从初等几何中具体的例子，我们分析了证明简洁性的定义方式。我们首先发现，当面对来自相互矛盾的假设集的两个证明时，如果可以做出判断，那么这个判断只能基于涉及的公理系统的形式方面之外的推理。然后我们证明，如果公理系统是固定的，那么可以根据被认为是深刻或有价值的公理的使用次数来定义证明简洁性的度量，并证明一些关于在其他证明中至少使用三次某些公理的必要性的新结果。一个这样的主要例子是帕普斯蕴涵德斯伽尔，它被证明需要三次使用帕普斯定律。在弗伦奇证明帕斯奇公理的外形式蕴涵内形式的过程中也遇到了类似的情况。任何这样的证明都至少需要三次使用外形式。我们还提到了证明的直接性和证明的长度之间可能存在的冲突要求。本文是主题为“简单证明的概念——希尔伯特第 24 个问题”的一部分。
