Regular logic

Regular logic has atomic formulas and equality, truth, finite conjunction and unrestricted existential quantification. Its categorical semantics uses regular categories: conjunction is intersection and existential quantification is image. Disjunction and falsity are not added as formula constructors in the regular fragment.

A regular theory has axioms that are sequents between regular formulas. It has a regular syntactic category and a classifying topos of sheaves for the regular coverage. Its regular formulas enjoy the disjunction property of regular theories when a finite disjunction is allowed as an outer coherent conclusion.

Classically, a regular formula sequent that is not provable has a set-valued countermodel, with empty sorts allowed. Start with the finite diagram of its antecedent, successively adjoin witnesses to the existential consequences of each axiom, and identify elements when equality axioms require it. Every new fact about the original parameters has a finite derivation, so the nonderivable consequent remains false. The filtered union of this witness construction is a model. The conservativity property of this chase construction is studied in Forssell and Lumsdaine's paper.

If a regular theory proves an outer coherent sequent $\varphi ⊢{\bigvee }_{i=1}^n{\psi }_i$ with all formulas regular, it proves $\varphi ⊢{\psi }_i$ for some $i$. In the classifying topos, the corresponding subobjects cover the representable associated with $\varphi$. Irreducibility of that representable and full faithfulness of the syntactic Yoneda embedding produce the desired derivation.

The regular syntactic category has regular formulas-in-context as objects and provably functional regular relations as arrows. It has finite limits and stable image factorizations, with existential quantification supplying images. The regular coverage on this category presents the classifying topos of the theory.

A regular formula is built using the constructors of regular logic, with a finite variable context. The image of a definable relation interprets an existential quantifier. Regular formulas remain regular after substitution, conjunction and existential quantification.