Abstract
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.
Original language  English (US) 

Article number  Y 
Journal  Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 
Volume  377 
Issue number  2140 
DOIs  
State  Published  Mar 11 2019 
Keywords
 Direct proof
 Elementary geometry
 Hilbert’s 24th problem
 Multiple uses of axioms
 Ordered geometry
 Simple proofs
ASJC Scopus subject areas
 General Mathematics
 General Engineering
 General Physics and Astronomy
Fingerprint
Dive into the research topics of 'Prolegomena to any theory of proof simplicity'. Together they form a unique fingerprint.Datasets

Pythagorean theorem from Prolegomena to any theory of proof simplicity
Pambuccian, V. (Contributor), figshare Academic Research System, Jan 1 2018
DOI: 10.6084/m9.figshare.7435553.v1, https://doi.org/10.6084%2Fm9.figshare.7435553.v1
Dataset

Pappus axiom from Prolegomena to any theory of proof simplicity
Pambuccian, V. (Contributor), figshare Academic Research System, Jan 1 2018
DOI: 10.6084/m9.figshare.7435544.v1, https://doi.org/10.6084%2Fm9.figshare.7435544.v1
Dataset