throwaway982736

Does this help?:

https://medium.com/@IsaacSimpson/urbit-and-the-not-so-dark-f...

"So it's not true that Tlon can't just say $user's compute node is hereby expelled?"

Correct, this is untrue.

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