|
|
|
|
|
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." |
|