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 geometric. 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 logic has good proof theory. Entailment is semi-decidable, decidable only in the function-free existential-free case. Complete for coherent topos semantics. Many mathematical theories (lattices, groups, fields) coherent. Automated provers exist (coherent prover). Barr's theorem: classical ⊢ coherent theorem → intuitionistic proof.

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

Limitations. Cannot express full first-order logic. No implication or negation in formulas. Universal quantification only implicit in sequents. Less expressive than full FOL. Not widely known outside specialists.

© 2026 Lingenic LLC