*I* think that there’s a flaw in the argument.

I could elaborate, but maybe you want to think about this more, so for now I’ll just address your remark about , where is refutable. If we assume that , then, since is false, must be false, so must be true. That is, you have proven that PA proves , that is, since is contradictory, PA proves its own inconsistency. You’re right that this is compatible with PA being consistent—PA may be consistent but prove its own inconsistency—but this should still be worrying.

Theorem. Weak HCH (and similar proposals) contain EXP.

Proof sketch: I give a strategy that H can follow to determine whether some machine that runs in O(2cnk) time accepts. Basically, we need to answer questions of the form “Does cell x have value y at time t.” and “Was the head in position x at time t?”, where x and t are bounded by some function in O(2cnk). Using place-system representations of x and t, these questions have length in O(nk), so they can be asked. Further, each question is a simple function of a constant number of other such questions about earlier times as long as t>0, and can be answered directly in the base case t=0.