A book picked at random off a shelf in the library of Mathematisches Forschungsinstitut Oberwolfach and opened at a random page revealed a little gem, a paper by Pierre Ageron Logic without self-deductibility, in: Logica Universalis (J.-Y. Beziau, ed.), Birkhauser, Basel – Boston -Berlin, 2007, pp. 87-93.
The “law of self-deductibility” is a simple principle “if A, then A” which expresses the reflexivity of entailment; apparently, its formulation can be traced back to Stoic philosophers. Pierre Ageron comments that
Self-deductibility has a paradoxical status. It seems so obvious that, unlike the law of exluded middle [...] it has hardly ever a matter of controversy [...]. Also it seems of no use whatsoerver in the mathematical practice and totally sterile in terms of deductive power.
However, then Pierre Ageron points out that Charles Pierce in hisAlgebra of Logic (1885)
mentions in passing quite a remarkable interpretation of the law of self-deductibility. Pierce referes to it as the “first icon of algebra” and argues that it “justifies our continuing to hold what we have held, though we may, for instance, forget how we were originally justified in holding it”. This clearly suggests that self-deductibility works as an amnesia principle: once some statement is proved, it allows us to forget how it was proved. In mathematical practice, it is obviously a good thing that we can continue to trust our old theorems even if we are unable to reconstruct their proofs.
In my book, I briefly discuss Timothy Gowers‘ observation that, in his opinion, a “comprehensible” proof is not necessarily the shortest one, but a proof of small width. Here, width measures how much you must hold in your head at any one time. Alternatively, imagine that you write a detailed proof on a blackboard, carefully referring to all intermediate steps.
However, if you know that a certain formula or lemma will never be used again, you erase it and re-use the space. A “small width” proof is a proof which never expands beyond one (small) blackboard. In other words, a “comprehensible” proof is a proof produced by a systematic application of the “amnesia principle” and the humblest of all tautologies, “if A then A”.
[Imported from my old and now defunct blog]