Tuesday, January 31, 2017

Godel's Construction for Humans

Part I: Setup
One day, our favorite neighborhood superintelligent game-theoretic agent Omega sits me down and says “John, let’s play a game.”

“I’ve written a simulation of you,” says Omega, “and before we get to the main game, I need to calibrate it. There’s a few parameters which need to be matched in order to properly simulate you.”

“Ok,” I reply, “What do I need to do?”

“I need you to prove this theorem,” says Omega, “while you work on proving it, I will simulate you proving the theorem, and make sure that the simulation output matches your own proof.” She hands me a piece of paper which (translated from math to english) reads “There exist infinitely many prime numbers.”

This is a classic problem, so I pull out my pencil and quickly write down a simple proof. When I’m done, Omega checks the paper, then checks her computer, and smiles.

“The simulation matches!” Omega announces. “All of the parameters fit, and now we can perfectly simulate you. Now, while I set up the main game...” Omega hands me few pages of paper.

Part II: Introspection
“Read through that carefully,” says Omega, “It contains a full specification of the simulation of you.” She hands me one more piece of paper. “These are the parameters we just calibrated, so now you have everything needed to run a simulation of yourself.”

I look at the papers and frown. It’s shorter than I would have liked.

I start flipping through. Omega’s models are, as usual, quite elegant. Looking at the fifth page, I grab a piece of mail off the table and run a quick back-of-the-envelope calculation. The result outlines a dream I had the night before with tiny multicolored lobsters pinching at my feet. Another calculation predicts that my blood sugar is a bit low… I grab a granola bar from my bag, then redo the calculation with time advanced by twenty minutes.

After I finish reading, I decide to try a slightly more complicated calculation. I check back a few pages, and find what I’m looking for: the specification for an infinite lazy data structure which encodes me, calculating a simulation of myself calculating a simulation of myself calculating a simulation of myself calculating…

“Ready!” says Omega, breaking my infinite regress. “Have you figured out that simulation specification?”

“I think so,” I reply, “it’s surprisingly understandable. Very elegant.”

“Thank you,” replies Omega. “On to the main game!”

Part III: The Game
Omega hands me another single sheet of paper. “Please prove this theorem,” she says.

I look at the sheet. It shows a data structure which refers back to the me-simulation spec. I flip back and forth for a minute, decoding the contents of the new paper, until I realize what it says:

“John cannot prove this theorem.”

I stop. It’s an impressive piece of work. First, a full, perfect mathematical specification of myself. Then, a shorter statement claiming that, based on the mathematical specification of me, I cannot prove the theorem. If I do prove the theorem, then I’ve proven that I can’t do it…

Wait! Technically, this just claims that the *simulation* of me can’t prove the theorem. So if the simulation is inaccurate, I might still be able to - I slap my forehead. No, this is Omega I’m dealing with. She’s scrupulously honest, and her simulations have never once been wrong. This is an accurate specification of me.

For all intents and purposes, I’m dealing with a copy of myself. If I can prove this theorem, then so can the simulation. But the statement says “John cannot prove this theorem.” If it’s false, then I *can* prove it, but then I’d be proving something false, so my proof would be wrong, so the theorem would be true… And if it’s true, then I can’t prove it.

I grumble a bit. It’s a classic diagonalization gambit. There’s no way I can prove this theorem… unless...

Part IV: Breaking Out
The only way I can prove this theorem is if I can somehow make the simulation *not* match myself. I mean, the simulation specifies a perfect copy of me, but if I could use some information which the simulation doesn’t have… Smiling slightly, I reach into my pocket, and withdraw a q-coin.

“A quantum random coin,” says Omega, “very clever.”

I catch a hint of sarcasm. “You knew full well I was going to use this, didn’t you?”

“Of course,” replies Omega, “The simulation is also using a q-coin. You haven’t actually diverged from it yet.”

“But once I flip this, I will,” I say, “It’s perfect randomness. The simulation can predict that I’ll flip it, and it can even simulate all possible outcomes, but it won’t know which outcome I actually get.”

Omega smiles as I flip the q-coin. Heads. I flip it again. Tails. I keep flipping. Heads-heads-heads-heads-tails-heads-tails…

Eventually, I turn back to the math. Sure enough, the simulation specifies a full distribution over all possible outcomes of the coin flip. I start to think about how to finally prove that theorem…

“Crap,” I say.

“Yup,” replies Omega.

“I’ve diverged from the simulation, but those coin flips don’t actually have a significant causal impact on my ability to prove the theorem. The theorem-proving part of the system isn’t chaotic enough to be affected by coin flips. There’s a whole distribution in there for the outcome of the flips, but that distribution isn’t relevant to theorem-proving.”

I lean back and close my eyes. If I want the coin-flips to affect theorem-proving, then I need some way to leverage randomness of the flips in the proof itself...

No comments:

Post a Comment