4 ms·
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
by throwaway982736 10y 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."