|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-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|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, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
In principle also all other notions of theory, such as in the sense of physics should be special cases of this, but in practice of course there are many systems called “theories” which are not (yet) as fully formalized as in mathematical logic.
There are several different viewpoint on theories:
is that the theory itself consists of a set of formulas in the first order language of a signature . Classically, these formulas are assumed to have no free variables (i.e. to be “sentences”), but in weaker logics that lack universal quantification it is better to take them to be formulas-in-context. One also sometimes considers the theory to also include all logical consequences (aka theorems) of the axioms in , relative to (some specified) fragment of first-order logic — that is, to be “saturated” with respect to provability.
that preserve some (typically property-like) structures on , such as certain classes of colimits or of limits, pertinent to the fragment of logic at hand. Then a completeness theorem would be the statement that the canonical map
is a full faithful embedding (one that preserves all relevant logical structure). For this reason, completeness theorems are also known as embedding theorems.
Hm, is that the way it should be said?
In fact, the notion of model can be generalized away from to more general categories, namely those that have enough structure to “internalize” the fragment of logic at hand. From this very general point of view on model, the syntactic category is the generic or universal model for , and if we simply call the theory, then models and theories are placed on the same footing.
In this article we mostly consider the categorical view on “theory”.
In first-order logic, a theory is presented by
For instance (Johnstone, def. D1.1.6).
There are many different kinds of “theory” depending on the strength of the “logic”: a by-no-means complete list includes
first-order logic (aka pretopos logic),
and corresponding theories for these logics.
There is a hierarchy of theories that can be interpreted in the internal logic of a hierarchy of types of categories. Since predicates in the internal logic are represented by subobjects, in order to interpret any connective or quantifier in the internal logic, one needs a corresponding operation on subobjects to exist in the category in question, and be well-behaved. For instance:
geometric theories Finally, theories which also involve infinitary , which is again represented by an infinitary union, can be interpreted in infinitary coherent categories, aka geometric categories. These are geometric theories.
Note that the axioms of one of these theories are actually of the form
where and are formulas involving only the specified connectives and quantifiers, means entailment, and is a context. Such an axiom can also be written as
so that although and are not strictly part of any of the above logics, they can be applied “once at top level.” In an axiom of this form for geometric logic, the formulas and which must be built out of , , , , and are sometimes called positive formulas.
Interestingly, one form of logic which made an early appearance but is not ordinarily thought of as logic at all is the logic of abelian categories, which is characterized by certain exactness properties. Here a small abelian category can be thought of as a syntactic site for some “abelian theory”; models of the theory are exact additive functors with domain . The classical models would in fact be exact additive functors , or exact additive functors to a category of modules. A “Freyd-Heron-Lubkin-Mitchell” embedding theorem is then a completeness theorem with respect to the classical models, and assures us that a statement in the language of abelian category theory is provable if and only if it is true when interpreted in any module category.
The simplest nontrivial theory is the
A still pretty simple but very nontrivial theory is
are discussed at fully formal ETCS.
The basic concept is of a structure for a first-order language : a set together with an interpretation of in . A theory is specified by a language and a set of sentences in . An -structure is a model of if for every sentence in , its interpretation in , is true (“ holds in ”). We say that is consistent or satisfiable (relative to the universe in which we do model theory) if there exist at least one model for (in our universe). Two theories, , are said to be equivalent if they have the same models.
Given a class of structures for , there is a theory consisting of all sentences in which hold in every structure from . Two structures and are elementary equivalent (sometimes written by equality , sometimes said “elementarily equivalent”) if , i.e. if they satisfy the same sentences in . Any set of sentences which is equivalent to is called a set of axioms of . A theory is said to be finitely axiomatizable if there exist a finite set of axioms for .
A theory is said to be complete if it is equivalent to for some structure .
For instance the syntactic categories of Lawvere theories are precisely those categories that have finite cartesian products and in which every object is isomorphic to a finite cartesian power of a distinguished object . A model for a Lawvere theory is precisely a finite product preserving functor .
A standard textbook reference for the categorical semantics is section D of
A discussion of the relation between theories and their syntactic categories is at
Other references include
In Coq theories are specified with the