Conceptually, MIP* is extremely similar to IP, so if you understand the latter, you shouldn’t have a problem with MIP*. The entire point of an interactive protocol is that the verifier can become convinced of statements, without ever seeing an explicit line-by-line derivation (in this case, the actual ZFC contradiction) or being able to convince anyone else. All that matters is that the completeness and soundness conditions are satisfied. To review:

**Completeness:** If a given statement is true, then the prover(s) can act in a way that causes the verifier to accept with overwhelming probability.

**Soundness:** If a given statement is false, then no matter how the prover(s) act, the verifier will reject with overwhelming probability.

That’s it. In CS theory since the 1980s, any system whatsoever that satisfies the two conditions above, no matter how weird it looks otherwise, gets to be dignified with the name “proof system.”

]]>With a polynomially bounded verifier even that doesn’t work. Am I missing something? “Show the contradiction” seems like “show the forced checkmate” in the claim Black has a forced win in chess. The amazing thing about IP is that it shows the existence of the forced win without actually outputting the whole game tree. So I thought the MIP* equivalent would only show existence since demonstrating would be unbounded in size.

]]>So in some sense, the more interesting question is whether MIP* provers could prove to you that ZFC is *consistent* (or more generally, that a given TM runs forever). As I said, the answer is not yet known. Having said that, there’s also a question about whether they could prove to you that a given TM halts, in time that can be upper-bounded by some computable function of the size of the TM, with no dependence on the TM’s running time. That’s also an open problem right now. Both of these problems are intimately connected to the Connes Embedding Conjecture, and to the equivalence or inequivalence of the two different notions of infinite entanglement.

But if the answers to the questions are yes, then there’s just a protocol that witnesses it, and (presumably) a proof of the protocol’s completeness and soundness that can be formalized in ZFC. In which case, an MIP* proof that a given TM halts is a proof that it halts, and a proof that it doesn’t is a proof that it doesn’t … in the real world. You don’t need to breathe a word about the formal figments of logic known as “nonstandard models of arithmetic,” any more than you would with ordinary zero-knowledge or interactive protocols, or for that matter with any other ordinary mathematical reasoning. It’s just a total irrelevancy.

]]>I still don’t see how it can work. Let’s say I believe ZFC is consistent, so there is no integer n that is the Gödel number of a proof of 1=0. But iIf all you and I can agree on about the integers is PA, then there *is* such an n in some (maybe nonstandard) model of PA. So we ask the MIP* verifier to settle the question and it says it says ZFC is inconsistent. How does it convince us there is an actual inconsistency rather than that the provers are working in a nonstandard model of arithmetic?

The theorems I was thinking of earlier were the “randomness doesn’t help computability” ones (e.g. by Sacks) mentioned in [this MO thread](https://mathoverflow.net/questions/58060) but I haven’t studied them.

]]>I am not making any of this up.

Sorry, if my question implied anything like that. It was just that I had similar expectations like asdf, and your answers indicated that those expectations for MIP* were inappropriate. So I tried to be careful and explain where my expectations came from.

In addition, it often turns out that my intuitive expectations about things related to probabilities are wrong. So I queried whether that was also the reason here why my expectations for MIP* were inappropriate.

(In order to get a better feeling for the power of randomness, I now worked through proofs of Adelman’s theorem and Toda’s theorem. Turns out I had worked through a proof of Adelman’s theorem before, and that PP and Toda’s theorem are actually much less about probability than I had expected. Guess I will have to work through proofs related to IP and MIP to get a better feeling for the power of randomness when it comes to proofs.)

]]>