Coherent logic

Coherent logic uses atomic formulas and equality, finite logical conjunctions and logical disjunctions, truth, falsity and existential quantification. Sequents are universally interpreted in a finite variable context. Its categorical semantics is provided by coherent categories, where conjunction is intersection, disjunction is finite union and existential quantification is image.

When $y$ is not free in $\theta$, the coherent quantifier obeys $\theta \wedge \exists y\varphi ⊣⊢\exists y(\theta \wedge \varphi )$. Categorically this is the interaction of existential images with pullback, ensuring stable image factorizations in a coherent category.

A coherent theory is a first-order signature with a set of coherent sequents as axioms. It has a coherent syntactic category containing a conservative syntactic model. Theories of groups, rings and integral domains admit coherent axiomatizations.

Objects are coherent formulas in context and arrows are provably total, single-valued relations, modulo provable equivalence. Composition existentially eliminates the intermediate tuple. Conjunction constructs finite limits, existential formulas construct images and disjunction constructs finite unions. It is a coherent category.

The canonical model interprets each sort as its truth-context object, each operation by its term graph and each relation by its atomic subobject. A coherent formula is interpreted by its own formula-in-context object. Consequently a coherent sequent holds in this model exactly when it is derivable in the theory.

A coherent sequent is an implication $\varphi {⊢}_{\vec{x}}\psi$ between coherent formulas in a common context. Its semantics is inclusion of the two interpreted subobjects of that context. The context is universally quantified outside the formulas.

A coherent formula is built from atomic relations and equality using $\top$, $\perp$, finite conjunction, finite disjunction and existential quantification. General negation and universal quantification are not constructors. Substitution of well-typed terms preserves coherent formulas.