= Solution
A <first-order signature> specifies sorts, function symbols with specified input and output sorts, and relation symbols with specified input sorts. A <coherent formula> is built from atomic relations and equalities using $\top$, $\bot$, finite <logical conjunctions>, finite <logical disjunctions>, and <existential quantification>. A <coherent theory> is a set of sequents $\phi\vdash_{\vec x}\psi$ between <coherent formulas> in a common finite context; its axioms are interpreted as universally closed implications. Neither general negation nor universal quantification is allowed inside <coherent formulas>.
One complete presentation of <coherent logic> consists of the following axiom and rule schemes, together with the theory's sequents. All displayed formulas have compatible sorts and contexts, and bound variables can be renamed.
Identity and cut give $\phi\vdash\phi$ and
$$
\frac{\phi\vdash\psi\quad\psi\vdash\theta}{\phi\vdash\theta}.
$$
Substitution replaces the free variables of any derivable sequent by well-typed terms, avoiding capture. Contexts can be enlarged by unused variables, and permuted or renamed.
The finite-meet rules are $\phi\vdash\top$, $\phi\wedge\psi\vdash\phi$, $\phi\wedge\psi\vdash\psi$, and
$$
\frac{\theta\vdash\phi\quad\theta\vdash\psi}{\theta\vdash\phi\wedge\psi}.
$$
The finite-join rules are $\bot\vdash\phi$, $\phi\vdash\phi\vee\psi$, $\psi\vdash\phi\vee\psi$, and
$$
\frac{\phi\vdash\theta\quad\psi\vdash\theta}{\phi\vee\psi\vdash\theta}.
$$
Include distributivity $\theta\wedge(\phi\vee\psi)\dashv\vdash(\theta\wedge\phi)\vee(\theta\wedge\psi)$.
Existential introduction is $\phi(\vec x,t)\vdash_{\vec x}\exists y\,\phi(\vec x,y)$. Existential elimination is
$$
\frac{\phi(\vec x,y)\vdash_{\vec x,y}\psi(\vec x)}{\exists y\,\phi(\vec x,y)\vdash_{\vec x}\psi(\vec x)},
$$
where $y$ is absent from $\psi$. Equivalently, the quantifier is <left adjoint> to weakening along the context projection. Include the <Frobenius rule in coherent logic>
$$
\theta(\vec x)\wedge\exists y\,\phi(\vec x,y)\dashv\vdash\exists y\,(\theta(\vec x)\wedge\phi(\vec x,y)).
$$
It can also be derived from the usual coherent natural-deduction rules.
Equality has $\top\vdash_x x=x$ and the substitution scheme
$$
x=y\wedge\phi(\vec z,x)\vdash_{\vec z,x,y}\phi(\vec z,y),
$$
including atomic formulas and terms of the signature. Symmetry, transitivity and congruence for all functions and relations follow. These schemes impose no unintended inhabitedness axiom on a sort.
The <coherent syntactic category> $\mathcal C_{\mathbb T}$ has objects formulas in context $[\vec x\mid\phi]$, up to renaming. An arrow from $[\vec x\mid\phi]$ to $[\vec y\mid\psi]$ is an equivalence class, modulo provable equivalence, of formulas $\theta(\vec x,\vec y)$ satisfying
$$
\theta\vdash\phi\wedge\psi,\qquad\phi\vdash_{\vec x}\exists\vec y\,\theta,
$$
and
$$
\theta(\vec x,\vec y)\wedge\theta(\vec x,\vec y')\vdash\bigwedge_i y_i=y_i'.
$$
These are provably total functional relations. The identity is the equality graph restricted by $\phi$. If $\theta$ and $\rho$ are consecutive arrows, their composite is represented by $\exists\vec y\,(\theta\wedge\rho)$. Equality, cut and existential rules give the category laws.
A <coherent category> has <finite limits>, <pullback>-stable regular-epi/mono image factorizations, and finite unions of <subobjects> stable under <pullback>. We verify these structures syntactically. The <terminal object> is the empty-context truth formula. Products conjoin formulas in disjoint contexts; <equalizers> add equality of the two output tuples. For a functional relation $\theta$, its image in the target is represented by $\exists\vec x\,\theta$. Its factor onto that image is regular epic: two arrows out of the image agreeing on the source agree by existential elimination, and the same argument with the <kernel pair> gives the coequalizer property. Frobenius makes these image factorizations stable under <pullback>.
Every <subobject> of $[\vec x\mid\phi]$ is represented by a formula $\eta(\vec x)$ with $\eta\vdash\phi$. Indeed, take the existential image of a monic functional relation; uniqueness makes its map to that image an isomorphism. <Subobject> inclusion is exactly provable implication. Finite unions are consequently disjunctions, with bottom as the empty <subobject>; distributivity and substitution make them <pullback>-stable. Hence \b[$\mathcal C_{\mathbb T}$ is coherent].
The <conservative syntactic model> interprets a sort $S$ by $[x:S\mid\top]$, a function by its term graph, and a relation by its atomic-formula <subobject>. Induction on <coherent formulas> shows that $\phi(\vec x)$ is interpreted by the <subobject> $[\vec x\mid\phi]$ of its context object. It satisfies every theory axiom by construction. Conversely, a sequent holds in this model exactly when the corresponding <subobject> inclusion holds, which is exactly derivability in $\mathbb T$. Therefore
$$
\boxed{\text{the canonical model in }\mathcal C_{\mathbb T}\text{ is conservative}.}
$$
This is conservativity for <coherent sequents>, not a claim about non-<coherent formulas>.
Back to article page
