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. Decidable fragment with good computational properties.

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: ∃e.∀x.ex=x ∧ xe=x... (needs ∀, so axioms expressed as sequents)
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/existentials. Decidable for finite signatures, ground case.

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

Symbols.

Symbol	Unicode	Name	Meaning
∧	U+2227	Conjunction	And
∨	U+2228	Disjunction	Finite or
∃	U+2203	Exists	Existential
⊤	U+22A4	Top	True
⊥	U+22A5	Bottom	False
⊢	U+22A2	Sequent	Entailment

Metatheory. Coherent logic has good proof theory. Decidable for ground 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.