If you're interested in the details, you might want to have a look at papers [1] or [2]. You can add existentials in this framework, which basically means that

If you're interested in the details, you might want to have a look at papers [1] or [2]. You can add existentials in this framework, which basically means that the lifting problems mentioned above don't need to have unique solutions. But as you say, then the "minimal" databases aren't determined uniquely up to isomorphism anymore. So the result of Datalog evaluation now depends on the order in which you apply rules. If I recall correctly, then [3] discusses a logic corresponding to accessible categories (Datalog + equality corresponds to locally presentable categories) which includes the the theory of fields. The theory of fields involves the negation 0 != 1, so perhaps that might give you a nicer way to incorporate negations without stratification. [1] https://www.mbid.me/eqlog-semantics/ https://www.mbid.me/eqlog-semantics/ [2] https://arxiv.org/abs/2205.02425 https://arxiv.org/abs/2205.02425 [3] Locally presentable and accessible categories, https://www.cambridge.org/core/books/locally-presentable-and-accessible-categories/94CB48295B6AF097FC232313A57BDE17 https://www.cambridge.org/core/books/locally-presentable-and...