Hacker News new | ask | show | jobs
by throwaway982736 3361 days ago
Representing "Con(T)" in a formal language with the Peano Axioms isn't all that long, relatively speaking. No diagonalization is needed. It's basically:

~(Ex)Proof(x, ~0=0)

I.e., "There doesn't exist a proof of ~0=0."

Of course, representing the word "proof" using PA isn't trivial, and expanding that bulks things up a bit. But the sentence that's really long is the Godel sentence. "(G) There is no proof of G."