Articles by others on the same topic
The fragment uses finite conjunction, set-indexed disjunction and existential quantification, with equality and atomic relations. It is preserved under inverse image functors of geometric morphisms. The universal closure of an axiom is expressed by its variable context, not an unrestricted universal-quantifier constructor.