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.

Use the signature of unital commutative rings, its equational axioms, and the coherent sequents $0=1⊢\perp$ and $\top {⊢}_x\mathrm{Inv}(x)\vee \mathrm{Inv}(1-x)$, where $\mathrm{Inv}(x)$ abbreviates $\exists y(xy=1)$. In a set-based model the nonunits form its unique maximal ideal; this is the usual nonzero local ring. In a topos the disjunction expresses local existence of a unit witness. Its classifying topos is defined by the Zariski coverage on finitely presented rings.

A coherent sequent true in all set models of a coherent theory is coherently derivable. A generic underivable sequent remains false after the Boolean cover by a generic quasi-closed subtopos. Slice over its nonzero Boolean counterexample to show classical consistency of the theory with a named tuple satisfying the antecedent and negated consequent. The Henkin construction then gives a set-valued countermodel. This argument does not assume that every Boolean topos has points.

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.