nLab theory

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

---

Idea

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.

Definition

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(\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 $A$, 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_{\mathcal{T}}$, so that models of a theory $\mathcal{T}$ are identified with functors

  $$C_{\mathcal{T}} \to Set$$

  that preserve some (typically property-like) structures on $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_{\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 $Set$ 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_{\mathcal{T}}$ is the generic or universal model for $\mathcal{T}$, and if we simply call $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

Definition

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 $A$ of sequents of formulas in this signature, called the axioms of the theory: expressed in the first-order language $Lang(\Sigma)$ with equality generated by $\Sigma$

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

Semantic view

(…)

Categorical view

(…)

• categorical semantics

(…)

Examples

Classes of theories

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

• equational logic?,

• first-order theory

• Horn theory,

• essentially algebraic theory,

• geometric logic,

• regular logic,

• exact logic?,

• extensive logic?,

• coherent logic,

• first-order logic (aka pretopos logic),

and corresponding theories for these logics.

• essentially algebraic theory

• generalized algebraic theory

• algebraic theory

  • commutative algebraic theory

  • finitary algebraic theory: Lawvere theory

    • Fermat theory

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:

• cartesian theories Since $\wedge$ and $\top$ are represented by intersections and identities (top elements), these can be interpreted in any lex category. Theories involving only these are cartesian theories.

• regular theories Since $\exists$ is represented by the image of a subobject, it can be interpreted in any regular category. Theories involving only $\wedge$, $\top$, and $\exists$ are regular theories.

• coherent theories Since $\vee$ and $\bot$ are represented by union and bottom elements, these can be interpreted in any coherent category. Theories which add these to regular logic are called coherent theories.

• geometric theories Finally, theories which also involve infinitary $\bigvee$, 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

$$\varphi \vdash_{\vec{x}} \psi$$

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

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

• theory of objects

A still pretty simple but very nontrivial theory is

• elementary function arithmetic

• second order arithmetic

The theories

• $Th(Cat)$ of categories

• $Th(Lex)$ of finitely complete categories

• $Th(Topos)$ of elementary toposes

• $Th(ETCS)$ of sets (ETCS)

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 $L$: a set $M$ together with an interpretation of $L$ in $M$. A theory is specified by a language and a set of sentences in $L$. An $L$-structure $M$ is a model of $T$ if for every sentence $\phi$ in $T$, its interpretation in $M$, $\phi^M$ is true (“$\phi$ holds in $M$”). We say that $T$ is consistent or satisfiable (relative to the universe in which we do model theory) if there exist at least one model for $T$ (in our universe). Two theories, $T_1$, $T_2$ are said to be equivalent if they have the same models.

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

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

Categorical point of view and models in topoi

From the categorical point of view, for every theory $T$ there exists a category $C_T$ – the syntactic category $C_T$ – such that a model for $T$ is a functor $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^n$ of a distinguished object $x$. A model for a Lawvere theory is precisely a finite product preserving functor $C_T \to \mathcal{T}$.

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

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

Related concepts

• conservative extension

• algebraic theory, globular theory

• type theory

• theory of presheaf type

• ordinal analysis

• 2-theory, 3-theory

mathematical statements

• theory

• judgement, assertion

• hypothesis, consequence

• axiom

• assignment

• definition (inductive, coinductive)

• lemma

• proposition/type (propositions as types)

• theorem

• proof/program (proofs as programs)

• example, counterexample

• conjecture, folklore

• exercise

• analogy

• tautology

• paradox

References

• 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

• Peter Johnstone, Sketches of an Elephant

A discussion of the relation between theories and their syntactic categories is at

• n-category cafe 2010: what is a theory

Other references include

• Mamuka Jibladze, Teimuraz Pirashvili, Cohomology of algebraic theories, J. Algebra 137 (1991), no. 2, 253–296, doi

• wikipedia: list of first-order theories, Morley’s categoricity theorem, Decidability (logic), signature (logic)

In Coq theories are specified with the

• Gallina specification language.