Academic life has given me a lesson for the second time, and it was harsh this time.

The first lesson had a happy ending, and it can be described by the following words:

Beware of the paper bin!

This happened on 2008. I was experimenting with a really wonderful software, the bundle Prover9-Mace4, by the late Bill McCune. My aim was to obtain a family of examples of equational classes where some formula grows unboundedly in complexity (this formula was related to direct product representations).

So I set a parametrized family of equations, and get Prover9 to chase for some conclusions. No matter how big my parameter was, complexity would not surpass certain limit. I threw the whole family to the paper bin.

Later that month, I talked to my former advisor and said that those equations were rubbish. After he asked me why was that,  he told me, “Well, if the complexity is always bounded that could be a nice result!” I would have never thought like that: I was searching for something, and I obtained some lesser indication of the opposite. Would that be worth publishing? It was; actually, it made it into print in a record-breaking time.

The second lesson’s short version is the title of this post, and has very long time span. On 2003 I started giving lessons on propositional logic to 2nd-year students of CS. By 2006 I had some nice notes written, with a result about proofs by contradiction described in a previous post. In particular, I obtained the result: Any valid propositional formula of the form $\neg\phi$ can be proved without using the rule of contradiction.

When asked my former advisor if that was original, and he told me “That’s Glivenko’s theorem.” I was upset, and let the result sleep… for seven years. In that time (as a PhD student) I wouldn’t realize the interest of having an alternative proof published. It seems that it took me all these years to learn this part of the lesson.

The last part is still fresh. After talking to some colleagues and browse the web in search of similar results, I finally decided to publish it. Sent it to the arXiv as usual.

Just today, Prof. Sara Negri from Helsinki informed me that this proof has already appeared in the book “Elements of logical reasoning” (CUP 2013) by Jan von Plato and uses a normalization result published in Normal derivability in classical natural deduction, Jan von Plato and Annika Siders, Review of Symbolic Logic, 2012.

I just withdrew my arXiv submission; wish that withdrawing some 6 idle years were that easy!