= Chase completeness for regular logic
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 https://arxiv.org/abs/1604.03851[Forssell and Lumsdaine's paper].
Back to article page
