In [*Categories for the working mathematician*, Ch. VIII, §4], Mac Lane introduces the **method of members** for interpreting diagram chases in an abelian category. We can (try to) generalise this to arbitrary regular categories as follows:

- A
**generalised element**of an object*X*is a morphism with codomain*X*. - Given two generalised elements of
*X*, say*x*_{0}and*x*_{1}, we define*x*_{0}=_{X}*x*_{1}to mean that there exist regular epimorphisms*e*_{0}and*e*_{1}such that*x*_{0}∘*e*_{0}=*x*_{1}∘*e*_{1}(in the usual sense of morphisms).

It is straightforward to see that *x*_{0} =_{X} *x*_{1} if and only if *x*_{0} and *x*_{1} have the same image in *X*, so generalised elements of *X* up to =_{X} are the same as subobjects of *X* up to isomorphism.

We can then prove this lemma:

**Lemma.** A morphism *f* : *X* → *Y* is a regular epimorphism if and only if, for each generalised element *y* of *Y*, there exists a generalised element *x* of *X* such that *f* ∘ *x* =_{Y} *y*.

The obvious next thing to try to prove is the following:

**Claim.** A morphism *f* : *X* → *Y* is a monomorphism if and only if *f* ∘ *x*_{0} =_{Y} *f* ∘ *x*_{1} implies *x*_{0} =_{X} *x*_{1}.

It is certainly true if the category is abelian (cf. Mac Lane), and it is also true when there are “enough subterminal objects” (e.g. sheaves on a topological space). Unfortunately it is false in general. Given a non-trivial group *G*, the category of *G*-sets is a regular category (indeed, a topos), but the unique morphism *G* → 1 is not a monomorphism despite satisfying the condition on generalised elements.

One way of repairing this is to abandon the equivalence relations =_{X}. This leads to the forcing semantics for regular logic in regular categories. Roughly:

*U*⊩*x*_{0}=_{X}*x*_{1}means that*x*_{0}and*x*_{1}are equal as morphisms*U*→*X*.*U*⊩*φ*∧*ψ*means that both*U*⊩*φ*and*U*⊩*ψ*hold.*U*⊩ ∃*x*:*X*.*φ*, where*x*is a free variable in*φ*, means that there exist a regular epimorphism*e*:*V*→*U*and a morphism*x*:*V*→*X*such that*V*⊩*e***φ*, where*e***φ*is the result of replacing every generalised element*y*appearing in*φ*with*y*∘*e*.*U*⊩*φ*⇒*ψ*means that, for any morphism*f*:*V*→*U*,*V*⊩*f***φ*implies*V*⊩*f***ψ*.

Note that ⇒ is not a logical connective in regular logic, so it can only appear in the outermost level. Under this interpretation, given a morphism *f* : *X* → *Y*, we have *Y* ⊩ ∃*x* : *X*. *f* ∘ *x* =_{Y} id_{Y} if and only if *f* is a regular epimorphism, and *X* × *X* ⊩ *f* ∘ *x*_{0} =_{Y} *f* ∘ *x*_{1} ⇒ *x*_{0} =_{X} *x*_{1}, where *x*_{0}, *x*_{1} : *X* × *X* → *X* are the two projections, if and only if *f* is a monomorphism.

However, one is left wondering whether there might be a simplification of the forcing semantics that does not require us to keep track of the domains of our generalised elements, as in the method of members.

Just for the record, not keeping track of the domains prevents constructing morphisms using the naive element-based language (as opposed to merely verifying some properties of already-given morphisms). This happens even in the abelian case.