is the fragment of first-order logic that can express statements of the form

where and are regular formulae i.e. formulae built up from atomic formulae, the truth constant, binary meets (conjunction) and existential quantification. Such formulae can be interpreted in a regular category, and the