|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-level 1-type/h-prop|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
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.
In full first-order logic, such a sequent is equivalent to the single formula
\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 and a string of s at the very outer level of a formula.
Any (finitary) algebraic theory is coherent.
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; a similar example is the theory of a discrete field.
The theory of a linear order is (seemingly) not coherent: the “connectedness” axiom is not coherent since negation is not allowed in coherent formulas. We can express one outer negation, however, as in the irreflexivity axiom .
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 and in classical logic). See D1.5.9 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 , in a natural way, then that relation is named by some coherent formula in . 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 , 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 the conceptual completeness theorem; 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 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.
Sometimes coherent logic is called geometric logic, but that term 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.
Occasionally the existential quantifiers in coherent logic are further restricted to range only over finitely presented types.