Prolegomena to any theory of proof simplicity

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'.