nLab coherent logic

Coherent logic


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Coherent logic


Coherent logic is a fragment of (finitary) first-order logic which allows only the connectives and quantifiers

A coherent formula is a formula in coherent logic.

A coherent sequent is a sequent of the form φψ\varphi \vdash \psi, where φ\varphi and ψ\psi are coherent formulas, possibly with free variables x 1,,x nx_1,\dots,x_n.

In full first-order logic, such a sequent is equivalent to the single formula

x 1,,x n(φψ) \forall x_1, \dots, \forall x_n (\varphi \Rightarrow \psi)

(in the empty context). Of course, this latter formula is not coherent, but this shows that when we deal with coherent sequents rather than merely formulas, it can also be thought of as allowing one instance of \Rightarrow and a string of \foralls at the very outer level of a formula.

Coherent logic (including sequents, as above) is the internal logic of a coherent category. The classifying topos of a coherent theory is a coherent topos.


  • Any (finitary) algebraic theory is a coherent theory, as is any theory in regular logic. Syntactically this is obvious, as algebraic theories and regular theories use only a fragment of the logical connectives available in coherent logic. However, it should be noted that the syntactic category of an algebraic theory is not the same as its syntactic category when regarded as a coherent theory: the latter is the “free coherent category” generated by the former (which is a category with finite products).

  • A good example of a coherent theory that is not algebraic (in any of the usual senses, although it comes from algebra) is the theory of a local ring, defined by axioms 0=10 = 1 \vdash \bot and

    x+y=1(z.xz=1)(z.yz=1)x + y = 1 \vdash (\exists z.x \cdot z = 1) \vee (\exists z.y \cdot z = 1)
  • The theory of a totally ordered set is another example of a coherent theory that is not algebraic. One adds to the algebraic theory of a idempotent commutative semigroup the totality axiom x,y(xy=x)(xy=y)\vdash_{x,y} (x \sqcup y = x) \vee (x \sqcup y = y).

  • Similar examples are the theories of a discrete field.

  • The theory of an apartness relation is coherent. The irreflexivity axiom is expressed as (x#x)(x \# x) \vdash \bot, the symmetry axiom is expressed as (x#y)(y#x)(x \# y) \vdash (y \# x), and the comparison axiom is expressed as (x#z)y.(x#y)(y#z)(x \# z) \vdash \exists y.(x \# y) \vee (y \# z). However, the “tightness” axiom ¬(x#y)(x=y)\neg(x\# y) \vdash (x=y) in tight apartness relations is not coherent since it uses negation.

  • The theory of a total order is coherent, though also not algebraic. The theory of a partial order is essentially algebraic, but the totality axiom x,y(xy)(yx)\vdash_{x,y} (x\le y) \vee (y\le x) is coherent but not essentially algebraic.

  • The theory of a strict total order is not coherent if we use the “connectedness” axiom (xy),(yx)(x=y)(x\nless y), (y\nless x) \vdash (x=y), which is not coherent since negation is not allowed in coherent formulas. We can express one outer negation, however, as in the irreflexivity axiom (x<x)(x\lt x)\vdash \bot. In classical mathematics, there is another solution, to use the “trichotomy” axiom (x=y)(x<y)(y<x)\top \vdash (x=y) \vee (x\lt y) \vee (y\lt x) instead, in order to get an axiomatisation of “coherent” strict total orders. However, in constructive mathematics, strict total orders are in general not trichotomous, so this solution cannot be used.

  • The theory of a strict weak order is coherent, since it doesn’t have the connectedness axiom that strict total orders do. The irreflexivity axiom is expressed as (x<x)(x\lt x)\vdash \bot, and the asymmetry axiom is expressed as (x<y)(y<x)(x \lt y) \wedge (y \lt x) \vdash \bot.

  • Since the theory of a local ring and a strict weak order is coherent, this means that the theory of an ordered local ring is also coherent, where we have

    (x<y)(y<x)z.yz=1+xz(x \lt y) \vee (y \lt x) \vdash \exists z.y \cdot z = 1 + x \cdot z


    z.xz=1(0<x)(x<0)\exists z.x \cdot z = 1 \vdash (0 \lt x) \vee (x \lt 0)
  • The theory of a reduced ring is coherent, with the trivial nilradical axiom being expressed as xx=0x=0x \cdot x = 0 \vdash x = 0.

  • Similarly, the theory of an integral domain is coherent, with the zero-product property? axiom being expressed as (xy=0)(x=0)(y=0)(x \cdot y = 0) \vdash (x = 0) \vee (y = 0)

  • Since GCD rings and Bézout rings are algebraic theories and integral domains are coherent, GCD domains and Bézout domains are coherent as well.

  • The theory of an elementary topos is coherent. However, the well-pointedness condition for a well-pointed topos is not coherent, which means that the theory ETCS is not coherent. See fully formal ETCS for more details.


Coherent logic has many pleasing properties.

  • Every finitary first-order theory is equivalent, over classical logic, to a coherent theory. This theory is called its Morleyization and can be obtained by adding new relations representing each first-order formula and its negation, with axioms that guarantee (over classical logic) these relations are interpreted correctly (using the facts that (PQ)(¬PQ)(P\Rightarrow Q) \dashv\vdash (\neg P \vee Q) and (x,P)(¬x,¬P)(\forall x, P) \dashv\vdash (\neg \exists x, \neg P) in classical logic). See D1.5.13 in Sketches of an Elephant, or Prop. 3.2.8 in Makkai-Paré.

  • By (one of the theorems called) Deligne's theorem, every coherent topos has enough points. In particular, this applies to the classifying toposes of coherent theories. It follows that models in Set are sufficient to detect provability in coherent logic. By Morleyization, we can obtain from this the classical completeness theorem for first-order logic?. See for instance 6.2.2 in Makkai-Reyes.

  • Coherent logic also satisfies a definability theorem: if a relation can be constructed in every Set-model of a coherent theory TT, in a natural way, then that relation is named by some coherent formula in TT. See chapter 7 of Makkai-Reyes or D3.5.1 in Sketches of an Elephant.

  • It follows that if a morphism of coherent theories (i.e. an interpretation of one coherent theory in another) induces an equivalence of their categories of models in SetSet, then it is a Morita equivalence of theories (i.e. induces an equivalence of classifying toposes, hence an equivalence of categories of models in all Grothendieck toposes). This is called conceptual completeness; see 7.1.8 in Makkai-Reyes or D3.5.9 in Sketches of an Elephant. (Note, though, that two coherent theories can have equivalent categories of models in SetSet without being Morita equivalent, if the former equivalence is not induced by a morphism of theories; see for instance D3.5.4 in the Elephant.)

However, here is a property which one might expect coherent theories to have, but which they do not.

  • The category of models of a coherent theory (in Set) is always an accessible category (this is true more generally for models of any logical theory). However, it need not be finitely accessible (i.e. ω\omega-accessible). An example is given in Adamek-Rosicky 5.36: the theory of sets equipped with a binary relation \prec such that for all xx there exists a yy with xyx\prec y. Then the model (,<)(\mathbb{N},\lt) of this theory does not admit any morphism from an (ω\omega-)compact object. (However, many coherent theories do have a finitely accessible category of SetSet-models.)


  • Sometimes coherent logic is called geometric logic, but that term is now more commonly used for the analogous fragment of infinitary logic which allows disjunctions over arbitrary sets (though still only finitary conjunctions). See geometric logic.

  • Conversely, geometric logic is sometimes called coherent , e.g. in Reyes (1977), so that coherent logic in the nLab terminology corresponds to the finitary fragment only.

  • Occasionally the existential quantifiers in coherent logic are further restricted to range only over finitely presented types.


An early reference is

  • M.-F. Coste, M. Coste, Théories cohérentes et topos cohérents , Séminaire de théorie des catégories dirigé par Jean Bénabou Mai 1975. (pdf)

A survey of results on geometric and coherent logic is in

  • Gonzalo Reyes, Sheaves and concepts: A model-theoretic interpretation of Grothendieck topoi , Cah. Top. Diff. Géo. Cat. XVIII no.2 (1977) pp.405-437. (numdam)

A standard textbook account of coherent logic (called ‘geometric logic’ there) can be found in

Properties of the generic model of a coherent theory are investigated in

Else consider the monographs

Last revised on December 26, 2023 at 06:17:07. See the history of this page for a list of all contributions to it.