So there exists a Turing machine (with some finite number of states N, naturally) that is just complex enough to encode ZF(C) and first-order logic such that it

So there exists a Turing machine (with some finite number of states N, naturally) that is just complex enough to encode ZF(C) and first-order logic such that it can enumerate all theorems of ZF(C). But because of Gödel, at some point it must necessarily either get stuck in a loop or return "can’t prove or disprove this" for some candidate theorem. As I understand it, the result relayed by Scott proves that N=7198 – as in a state space of merely 13 bits – is sufficient to construct a Gödel-territory TM (but this is just an upper bound)! Having an unbounded tape as a scratch space helps, of course.