There is one thing which really surprise me:
Page 44 (so 47 of the pdf
) he gives a “succ” relations, but he stated before that he does not want any order. And he certainly can obtain an order with the succ relation and the least fixed point.
And it is well known that you can compose LFP to obtain only one LFP, hence if it’s proof works, it should also works over structures with an order !
I do not state that it means that the proof is false, but if this works, it also implyes what look like to be a really strange corollary into finite model theory, because it would use a kind of locality which does not take care about the orders relation.
(At least that is what I understand of it but it may also be because this small part is really close to what was my current research)