According to https://link.springer.com/article/10.1007%2Fs001530050135 (Logics that define their own semantics, Imhof 1999) the logic FO[LFP] can define its own semantics, though the proof (of corollary 6.4) is somehow fuzzy. It is known from finite model theory that Datalog is equivalent to FO[LFP] (on ordered structures). Can someone help me see (at least partially) how to write a Datalog self-interpreter? The main difficulty is to express modus-ponens considering unification without involving existential variables in heads (i.e. variables in heads which don't appear in bodies and are understood to be existentially quantified).
Another related puzzle of mine is, if LFP's data complexity is P, and its query complexity is EXPTIME, how come it can interpret itself indeed? (I have no doubt that it can as the paper above supplied two different proofs for that. also we know that provably P!=EXPTIME)