= Regular-logic separation of a proper subobject
{title2=$S\hookrightarrow A\text{ proper}\Longrightarrow M(S)\subsetneq M(A)$}
For a <small category> that is a <regular category>, use a sort for each object, an operation for each <morphism>, and <regular theory> axioms describing <finite limits> and <regular epimorphisms>. Its models are <regular functors> into the <Category of sets>. For a proper <subobject> $m:S\hookrightarrow A$, the sequent asserting $\forall x:A\,\exists y:S,\ m(y)=x$ cannot be derivable, since its categorical interpretation would make $m$ a cover and hence invertible. The <chase completeness for regular logic> supplies a model where it fails. It is essential to allow empty sorts.
Back to article page
