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 time accepts. Basically, we need to answer questions of the form “Does cell have value at time .” and “Was the head in position at time ?”, where and are bounded by some function in . Using place-system representations of and , these questions have length in , 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 , and can be answered directly in the base case .
Here’s a simple Kripke frame proof of Payor’s lemma.
Let ⟨W,R,⊩⟩ be a Kripke frame over our language, i.e.W is a set of possible worlds, R is an accessibility relation, and ⊩ judges that a sentence holds in a world. Now, suppose for contradiction that W⊩x↔□(□x→x) but that W⊮x, i.e.x does not hold in some world u∈W.
A bit of De Morganing tells us that the hypothesis on x is equivalent to ¬x↔◊(□x∧¬x), so u⊩◊(□x∧¬x). So, there is some world v with uRv such that v⊩□x∧¬x. But again looking at our equivalent form for ¬x, we see that W⊩¬x→◊¬x, so v⊩□x∧◊¬x, a contradiction. □
Both this proof and the proof in the post are very simple, but at least for me I feel like this proof tells me a bit more about what’s going on, or at least tells me something about what’s going on that the other doesn’t. Though in a broader sense there’s a lot I don’t know about what’s going on in modal fixed points.
Kripke frame-style semantics are helpful for thinking about lots of modal logic things. In particular, there are cool inductiony interpretations of the Gödel/Löb theorems. These are more complicated, but I’d be happy to talk about them sometime.