nLab theory


This entry is about the notion in logic. For the notion of the same name in physics see at theory (physics).


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




In mathematical logic, a theory is a formal language used to precisely axiomatize a certain class of models.

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:

  • The

    syntactic view

    is that the theory itself consists of a set of formulas in the first order language Lang(Σ)Lang(\Sigma) of a signature Σ\Sigma. 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 include all logical consequences (aka theorems) of the axioms in AA, relative to (some specified) fragment of first-order logic — that is, to be “saturated” with respect to provability.

  • The

    semantic view

    is that the theory is given by the class of its models appropriate to that fragment of logic. Gödel’s completeness theorem is that a sentence in 𝒯\mathcal{T} is a theorem iff it is satisfied in every model.

  • The

    categorical view

    is that the logical formalism of a theory 𝒯\mathcal{T} can frequently be embodied in a syntactic category of terms C 𝒯C_{\mathcal{T}}, so that models of a theory 𝒯\mathcal{T} are identified with functors

    C 𝒯SetC_{\mathcal{T}} \to Set

    that preserve some (typically property-like) structures on C 𝒯C_{\mathcal{T}}, 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

    C 𝒯 modelsFinSetSetC_{\mathcal{T}} \to \prod_{models F in Set} Set

    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 SetSet 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 C 𝒯C_{\mathcal{T}} is the generic or universal model for 𝒯\mathcal{T}, and if we simply call C 𝒯C_{\mathcal{T}} the theory, then models and theories are placed on the same footing.

In this article we mostly consider the categorical view on “theory”.

Syntactic view


In first-order logic, a theory 𝒯\mathcal{T} is presented by

  1. a signature Σ\Sigma, specifying the allowed types of variables and the functions and relations between these;

  2. a set AA of sequents of formulas in this signature, called the axioms of the theory: expressed in the first-order language Lang(Σ)Lang(\Sigma) with equality generated by Σ\Sigma

For instance (Johnstone, def. D1.1.6).

Semantic view


Categorical view




Classes of theories

There are many different kinds of “theory” depending on the strength of the “logic”: a by-no-means complete list includes

and corresponding theories for these logics.

Hierarchy of theories: cartesian, regular, coherent, geometric

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:

Note that the axioms of one of these theories are actually of the form

φ xψ \varphi \vdash_{\vec{x}} \psi

where φ\varphi and ψ\psi are formulas involving only the specified connectives and quantifiers, \vdash means entailment, and x\vec{x} is a context. Such an axiom can also be written as

x.(φψ) \forall \vec{x}. (\varphi \Rightarrow \psi)

so that although \Rightarrow and \forall 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 φ\varphi and ψ\psi which must be built out of \top, \wedge, \bot, \bigvee, and \exists are sometimes called positive formulas.

Abelian theories

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 AA can be thought of as a syntactic site for some “abelian theory”; models of the theory are exact additive functors with domain AA. The classical models would in fact be exact additive functors AAbA \to Ab, 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.

Specific examples

The simplest nontrivial theory is the

A still pretty simple but very nontrivial theory is

The theories

are discussed at fully formal ETCS.

Models for a theory

Set-theoretic models for a first-order theory in syntactic approach

The basic concept is of a structure for a first-order language LL: a set MM together with an interpretation of LL in MM. A theory is specified by a language and a set of sentences in LL. An LL-structure MM is a model of TT if for every sentence ϕ\phi in TT, its interpretation in MM, ϕ M\phi^M is true (“ϕ\phi holds in MM”). We say that TT is consistent or satisfiable (relative to the universe in which we do model theory) if there exist at least one model for TT (in our universe). Two theories, T 1T_1, T 2T_2 are said to be equivalent if they have the same models.

Given a class KK of structures for LL, there is a theory Th(K)Th(K) consisting of all sentences in LL which hold in every structure from KK. Two structures MM and NN are elementary equivalent (sometimes written by equality M=NM=N, sometimes said “elementarily equivalent”) if Th(M)=Th(N)Th(M)=Th(N), i.e. if they satisfy the same sentences in LL. Any set of sentences which is equivalent to Th(K)Th(K) is called a set of axioms of KK. A theory is said to be finitely axiomatizable if there exist a finite set of axioms for KK.

A theory is said to be complete if it is equivalent to Th(M)Th(M) for some structure MM.

Categorical point of view and models in topoi

From the categorical point of view, for every theory TT there exists a category C TC_T – the syntactic category C TC_T – such that a model for TT is a functor C T𝒯C_T \to \mathcal{T} into some topos 𝒯\mathcal{T}, satisfying certain conditions.

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 x nx^n of a distinguished object xx. A model for a Lawvere theory is precisely a finite product preserving functor C T𝒯C_T \to \mathcal{T}.

We say a functor 𝒯 1𝒯 2\mathcal{T}_1 \to \mathcal{T}_2 of toposes (for instance a logical morphism or a geometric morphism) preserves a theory TT if for every model C T𝒯 1C_T \to \mathcal{T}_1 of TT in 𝒯 1\mathcal{T}_1, the composite C T𝒯 1𝒯 2C_T \to \mathcal{T}_1 \to \mathcal{T}_2 is a model of TT in 𝒯 2\mathcal{T}_2.

For instance, every geometric morphism preserves every Lawvere theory since, being a right adjoint, it preserves limits, hence finite products.

mathematical statements


  • H. Jerome Keisler, Fundamentals of model theory, A2 in JOhn Barwise, Handbook of mathematical logic (pp.47-103), North Holland 1977

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

Last revised on April 17, 2024 at 11:11:35. See the history of this page for a list of all contributions to it.