I only showed that the shortest proof of P(n) using Peano arithmetic is insanely long. I did provide a short proof of P(n). But I did this assuming Peano arithmetic is consistent!

So I didn’t give a short proof of P(n) using Peano arithmetic. I gave a short proof using Peano arithmetic plus the assumption that Peano arithmetic is consistent!

So, if we add to Peano arithmetic an extra axiom saying ‘Peano arithmetic is consistent’, infinitely many theorems get vastly shorter proofs!

This is often called Gödel’s speedup theorem.

— Insanely Long Proofs

— John Baez

2013.03.18 Monday ACHK