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]

### Like this:

Like Loading...

*Related*

In Linear Logic, one may only have a finite number of each propositional (or other logical) symbol to use in a proof. Thus, at a particular step in a proof we may know that A is true, but this does not necessarily mean we can, at a subsequent proof step, conclude A, since we may have already exhausted our stocks of the symbol “A”.

These ideas are so contrary to most (modern, western) mathematical notions, that most readers of this post will find them counter-intuitive. Linear logic has applications, however, to domains such as computer science where resources, and their modeling and husbandry, are important.

By:

peteron November 20, 2011at 8:13 pm

As an example, the law of self-deducibility and standard Modus Ponens would sanction the following theorem:

Premises:

A

If A then B

Conclusions:

A

B.

However, suppose A = “I have eggs” and B = “I have an omelette”. In this case, the creation of B may exhaust the resources represented by A.

By:

peteron November 20, 2011at 8:34 pm