I learned this morning that the double negation interpretation of classical logic in intuitionistic logic originates with Kolmogorov, not Gödel. However, arguably this is mostly just a result of isolated research communities.
I came across this while browsing through Paul Taylor's Practical Foundations of Mathematics late last night/morning. The reviews of it on Amazon are pretty harsh, but I can see that his presentation of the material can be distracting to readers who are coming at it with less context. I suppose you could say that he has a rather chatty style. One example that jumped out at me was some discussion at the beginning of Chapter 2 paralleling math and programming, with a sudden parenthetical aside on the fruitfulness of linear logic. It makes perfect sense to me, and actually gives it a kind of personable feel. But I can definitely imagine the uninitiated getting annoyed because they don't know what linear logic is about and it isn't really covered anywhere in the book. Regardless, I am rather tempted to buy the book.
I finally decided I should learn about this Knuth-Bendix algorithm I'm always hearing about, so I visited the math/physics library this morning to pick up Computational Problems in Abstract Algebra, which contains the originating paper: »Simple word problems in universal algebras«.