Coherent Logic

Origin. Emerged from the Grothendieck school's topos theory (SGA4, 1972); Makkai and Reyes, First Order Categorical Logic (1977), gave the model theory; Johnstone's Sketches of an Elephant (2002) is the reference. Bezem and Coquand (2005) revived it for automated theorem proving. Part of the geometric/coherent hierarchy from categorical logic. Formulas: atoms, ∧, ∨ (finite), ∃, ⊤, ⊥. No → or ∀ except in sequents. Preserved by inverse images of geometric morphisms. Semi-decidable, not decidable — see below.

Models. Positive existential formulas. Build from atoms using ∧, ∨, ∃ only. Sequents φ ⊢ ψ where both coherent. No negation or implication in formulas. Important: many mathematical theories coherent. Automated reasoning amenable.

Formalism.

Coherent formula: φ ::= ⊤ | ⊥ | R(t₁,...,tₙ) | φ ∧ ψ | φ ∨ ψ | ∃x.φ

No implication or universal quantification in formulas.

Coherent sequent: φ ⊢ₓ ψ (in context x, φ entails ψ)

Coherent theory: Set of coherent sequents as axioms.

Examples:

• Theory of groups: algebraic, the simplest case — with e and ⁻¹ in the signature the axioms are bare equations, ⊤ ⊢ₓ e·x = x and ⊤ ⊢ₓ x·x⁻¹ = e, needing neither ∃ nor ∀ in any formula. The universal quantification is carried by the context x of the sequent.
• Coherent axiom: ⊤ ⊢ ∃x.P(x)
• Coherent axiom: P(x) ∧ Q(x) ⊢ R(x)
• Coherent axiom: P(x) ⊢ Q(x) ∨ R(x)

Proof procedure: Forward chaining: apply sequents to derive atoms, branching on ∨ and introducing fresh witnesses for ∃. The procedure is complete, so coherent entailment is recursively enumerable — but it need not terminate, because each ∃ in a conclusion can introduce a new witness that fires the axioms again.

Semi-decidable, not decidable: Coherent entailment is undecidable. The regular fragment already contains definite Horn clauses over a signature with function symbols, and forward chaining there is Turing-complete, so no termination bound exists. What is decidable is the function-free, existential-free case — the Herbrand base is then finite and forward chaining saturates, which is the Datalog situation. The appeal for automated reasoning is therefore not decidability but proof quality: derivations are direct, need no Skolemization or clausal normal form, and read back as ordinary mathematical arguments — which is what Bezem and Coquand were after.

Regular logic: Restrict to ∧, ∃, ⊤ only (no ∨, ⊥). Even simpler fragment.

Symbols.

Metatheory. Coherent theories are the theories classified by coherent toposes, and models of T in a topos E correspond to coherent functors from the syntactic pretopos of T into E. Deligne's theorem (SGA4) — every coherent topos has enough points — is exactly the completeness theorem for coherent logic: a coherent sequent true in every Set-model of a coherent theory is derivable in the coherent calculus. Barr's theorem strengthens this constructively: any coherent sequent derivable from a coherent theory using classical logic and choice is already derivable intuitionistically, so classical proofs of positive statements can be mined for constructive ones. Makkai and Reyes proved conceptual completeness, that a coherent functor between pretoposes inducing an equivalence of model categories is itself an equivalence. Expressive power is not lost relative to first-order logic: Morleyization adds a relation symbol for each formula and turns any first-order theory into a coherent theory with the same models over the expanded signature, which is why coherent entailment is undecidable but recursively enumerable, with forward chaining as a complete but non-terminating procedure.

Applies to. Automated theorem proving. Mathematical formalization. Database queries (conjunctive + disjunctive). Ontology reasoning. Algebraic specification. Constructive algebra.

Limitations. The fragment is not closed under negation or implication. Negation is available only at the top level, as φ ⊢ ⊥, so there is no formula ¬φ to embed under ∨ or ∃, and universal quantification exists only as the implicit closure of a sequent's context — nested alternations of ∀ and ∃ cannot be written. Morleyization recovers full first-order expressiveness only by adding a relation symbol per formula together with the sequents R_φ ∧ R_¬φ ⊢ ⊥ and ⊤ ⊢ R_φ ∨ R_¬φ, the second of which postulates excluded middle, so the constructive content of Barr's theorem is lost in the encoding. Coherent theories are finitary: infinitary disjunction is excluded, so torsion abelian groups and similar theories are geometric but not coherent, and Deligne's enough-points theorem does not extend to them. Deligne's theorem is itself non-constructive, requiring a choice principle, and is unavailable in the constructive metatheories where Barr's theorem is wanted. Forward chaining is complete but non-terminating whenever conclusions contain ∃ over a signature with function symbols.

© 2026 Lingenic LLC