nLab
context

Idea

In logic, the context of an assertion (or judgement) consists of all of the assumptions that are made when that assertion is claimed to be valid; whether an assertion is in fact valid (or even meaningful) may depend on the context. The precise definition depends on the theory (or doctrine) that one is working in.

Generally, a context is thought of as relative to some underlying logical theory. This underlying theory will contain most of the assumptions of what constitutes validity; the context of an assertion in this theory will then include only those extra assumptions that may be used by that assertion. On the other hand, one could also think of the entire base theory as part of the context.

For example, in the theory of a group, it is understood that there is a group $G$, that $G$ has various elements, that two elements of $G$ may be equal, that any two elements of $G$ have as product an element of $G$, and that various equational laws are satisfied (which we will not list here). That is all taken for granted when discussing a group. However, the validity and meaningfulness of an assertion that two elements of $G$ commute will depend on (the rest of) the context.

To be more explicit, the assertion that $a$ and $b$ commute does not make sense without the additional context that $a$ and $b$ are elements of $G$. Even in that context, this assertion, while at least meaningful, is not valid. However, if we add to the context the assumption that $(ab{)}^2=a^2{b}^2$, then the assertion is valid. Written symbolically,

$$⊢ab=ba$$\vdash\; a b = b a

is meaningless;

$$a:G,b:G⊢ab=ba$$a\colon G,\; b\colon G \;\vdash\; a b = b a

is meaningful but invalid; and

(1)$$a:G,b:G,(ab{)}^2=a^2{b}^2⊢ab=ba$$a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2 \;\vdash\; a b = b a

is valid.

In a sufficiently rich logical language, contexts are unnecessary, which is why contexts are not usually explained in accounts of logic for ordinary reasoning (including in ordinary mathematics). For example, the two meaningful assertions above may be rewritten thus:

$$⊢\forall (a:G),\forall (b:G),ab=ba$$\vdash\; \forall (a\colon G),\; \forall (b\colon G),\; a b = b a

and

$$⊢\forall (a:G),\forall (b:G),(ab{)}^2=a^2{b}^2\Rightarrow ab=ba$$\vdash\; \forall (a\colon G),\; \forall (b\colon G),\; (a b)^2 = a^2 b^2 \;\Rightarrow\; a b = b a

Here the context on the left side is the empty context, consisting of no assumptions whatsoever (beyond those underlying the base theory).

However, these versions involve $\forall$ and $\Rightarrow$, while the previous versions work in weaker logics. In fact, these assertions make sense (and the valid one may be proved) in the internal logic of a group object in a finitely complete category (and somewhat more generally than that). Accordingly, they can be interpreted as statements about any group object in any finitely complete category (and the valid one will then be interpreted as a true statement), exactly as they do for groups (which are group objects in the finitely complete category Set).

Even if one is completely uninterested in internalization or weak logics, a basic familiarity with contexts may help drive home a point that is important throughout reasoning: What you can state and prove depends on your assumptions.

The category of contexts

Idea

Given a type theory $T$, it induces a category $\mathrm{Con}(T)$, whose

• objects are the contexts in the type theory;

• morphisms between contexts are substitutions, or interpretations of variables.

A morphism from the context $\Gamma$ to the context $\Delta$ consists of a way of fulfilling the assumptions required by $\Delta$ by appropriately interpreting those provided by $\Gamma$, generally by substituting terms available in $\Gamma$ for variables needed in $\Delta$ and proving whatever is necessary from the assumptions at hand.

This is called the category of contexts or category of contexts and substitutions of $T$.

A review is for instance in (Taylor section 2.8).

Definition

Let $\Gamma$ and $\Delta$ be contexts of some type theory $T$ of the form

$$\Gamma =x_0:A_0,x_1:A_1(x_0),x_2:A_2(x_0,x_1),\dots x_n:A_n(x_0,\dots ,x_{n-1})$$\Gamma \;=\; x_0:A_0,\; x_1:A_1(x_0),\; x_2:A_2(x_0,x_1),\;\dots x_n:A_n(x_0,\dots,x_{n-1})

and

$$\Delta =y_0:B_0,y_1:B_1(y_0),y_2:B_2(y_0,y_1),\dots y_m:B_m(y_0,\dots ,y_{m-1}).$$\Delta \;=\; y_0:B_0,\; y_1:B_1(y_0),\; y_2:B_2(y_0,y_1),\;\dots y_m:B_m(y_0,\dots,y_{m-1}) \,.

(Here we allow the possibility that each type in these contexts depends on the variables occurring earlier in the context, but for simplicity we can ignore that. )

Then a morphism $\Gamma \to \Delta$ in the category of contexts $\mathrm{Con}(T)$ consists of a sequence of terms such as the following:

$$\begin{array}{rl}\Gamma & ⊢t_0:B_0\\ \Gamma & ⊢t_1:B_1(t_0)\\ ⋮\\ \Gamma & ⊢t_m:B_m(t_0,t_1,\dots ,t_{m-1})\end{array}$$\begin{aligned} \Gamma &\vdash t_0 :B_0\\ \Gamma &\vdash t_1 : B_1(t_0)\\ \vdots\\ \Gamma &\vdash t_m : B_m(t_0,t_1,\dots, t_{m-1}) \end{aligned}

In other words, to give such a morphism we must give, for each type (or assumption) required by $\Delta$, a way to construct an element of that type (or a proof of that assumption) out of the data and assumptions contained in $\Gamma$.

This might fit better after the motivating examples below; but maybe those examples don't make sense to a newcomer. This is incomplete, however, since it doesn't address contexts that include equational hypotheses. —Toby

Properties

The category of contexts $\mathrm{Con}(T)$ has the universal property that for $C$ any suitable category, functors

$$\mathrm{Con}(T)\to C$$Con(T) \to C

that preserve the relevant structure correspond precisely to an interpretation of $T$ in $C$.

The construction

$$\mathrm{Con}:\mathrm{TypeTheories}\to \mathrm{Categories}$$Con\colon TypeTheories \to Categories

is the left adjoint in an adjunction that relates type theories and categories, whose right adjoint $\mathrm{Lan}:\mathrm{Categories}\to \mathrm{TypeTheories}$ extracts the internal logic of a category. See at type theory the section Categorical semantics.

Accordingly, the adjunction counit evaluated on any category $C$

$$\mathrm{Con}(\mathrm{Lan}(C))\to C$$Con(Lan(C)) \to C

says that there a canonical interpretatin of the internal logic of a category $C$ in $C$ itself. As it should be.

Examples

Substitution and introduction of a single term

Given a context $\Gamma$ and a type $X$, there is a new context $[\Gamma ,x:X]$.

Given a term $t:X$ there is a canonical morphism of contexts

$$\Gamma \stackrel{[t/x]}{\to }[\Gamma ,x:X]$$\Gamma \stackrel{[t/x]}{\to} [\Gamma, x : X]

which picks that term in $X$. The base change functor along this morphism

$$[t/x{]}^{*}:\mathrm{Con}(T{)}_{/[\Gamma ,x:X]}\to \mathrm{Con}(T{)}_{/\Gamma }$$[t/x]^* : Con(T)_{/[\Gamma, x : X]} \to Con(T)_{/\Gamma}

is the operation of substitution of variables: it sends a dependent type $\Gamma ,x:X⊢P(x)$ to $\Gamma ⊢P(t)$.

There is also the canonical morphism of contexts

$$\hat{x}:[\Gamma ,x:X]\to \Gamma$$\hat x : [\Gamma, x : X] \to \Gamma

which simply forgets the type $X$. The base change along this morphism is the context extension functor

$${\hat{x}}^{*}:\mathrm{Con}(T{)}_{/\Gamma }\to \mathrm{Con}(T{)}_{/[\Gamma ,x:X]}.$$\hat x^* : Con(T)_{/\Gamma} \to Con(T)_{/[\Gamma , x : X]} \,.

Its right adjoint is the dependent product functor ${\prod }_{x:X}$ giving the universal quantifier ${\forall }_{x:X}$, and its left adjoint is the dependent sum functor ${\sum }_{x:X}$ giving the existential quantifier ${\exists }_{x:X}$.

The theory of groups

For example, consider these contexts in the theory of a group $G$:

$$\Gamma =a:G,b:G$$\Gamma \;=\; a\colon G,\; b\colon G

$$\Delta =a:G,b:G,(ab{)}^2=a^2{b}^2$$\Delta \;=\; a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2

$$E=a:G,b:G,ab=ba$$E \;=\; a\colon G,\; b\colon G,\; a b = b a

$$Z=x:G,y:G$$Z \;=\; x\colon G,\; y\colon G

One interpretation of $\Gamma$ in $\Delta$ (that is, a morphism from $\Delta$ to $\Gamma$) is given by the substitution

$$a≔a,b≔b.$$a \coloneqq a,\; b \coloneqq b .

The fact that $(ab{)}^2=a^2{b}^2$ in $\Delta$ is ignored. In type-theoretic language, this would consist of the two terms

$$\begin{array}{rl}a:G,b:G,(ab{)}^2=a^2{b}^2& ⊢a:G\\ a:G,b:G,(ab{)}^2=a^2{b}^2& ⊢b:G\end{array}$$\begin{aligned} a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2 &\vdash a:G\\ a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2 &\vdash b:G \end{aligned}

Note that in this way of presenting things, the names of the variables in $\Gamma$ do not appear; only the order in which the types appear in $\Gamma$ matters.

A less obvious interpretation of $\Gamma$ in $\Delta$ is the substitution

$$a≔b,b≔a.$$a \coloneqq b,\; b \coloneqq a .

There is no reason to keep variable names the same. (At this point, compare $\Gamma$ and $Z$; when the definition is complete, it ought to follow that these are isomorphic.)

Another, perhaps even less obvious, morphism $\Delta \to \Gamma$ is

$$a≔a^2,b≔a^3.$$a \coloneqq a^2,\; b \coloneqq a^3 .

Not only does this ignore that $(ab{)}^2=a^2{b}^2$; it also ignores the very existence of $b$ in $\Delta$. (It also uses the existence of $a$ more than once. Ignoring and reusing information like this is not always allowed in substructural logics such as linear logic.)

That we can interpret $E$ in $\Delta$ without renaming variables is essentially the meaning of the judgement (1) above. That is, we get a morphism from $\Delta$ to $E$ by performing the substitution

$$a≔a,b≔b$$a \coloneqq a,\; b \coloneqq b

and then inserting a proof of (1). As it happens, the argument in such a proof is reversible, so you should expect that $\Delta$ and $E$ are also isomorphic.

Are there any morphisms from $\Gamma$ to $\Delta$? The obvious substitution does not define a morphism, since the required fact cannot be proved. However, you get one using the substitution

$$a≔a,b≔a$$a \coloneqq a,\; b \coloneqq a

and then inserting a proof that

$$\Gamma ⊢(aa{)}^2=a^2{a}^2.$$\Gamma \;\vdash\; (a a)^2 = a^2 a^2 .

All the same, we would not want to say that $\Gamma$ and $\Delta$ are isomorphic contexts; although there are morphisms in each direction, composing them should never produce identity morphisms on both sides.

Now I should finish defining the category. First, given a context $\Gamma$, there is an obvious identity morphism where every variable is substituted for itself and every statement assumed is proved immediately from itself.

Given morphisms $\Gamma \stackrel{f}{\to }\Delta \stackrel{g}{\to }E$, form the composite as follows: First, for each variable $X$ required by $\Gamma$, $f$ tells us how to substitute a term $T$ built out of the variables in $\Delta$, while $g$ tells us how to substitute a term from $E$ for each of these variables. So in the end, $X$ is expressed as a term $T[g]$ involving variables available in $E$. Also, by combining the proofs provided by $f$ and $g$, we get the proofs required for their composite.

To really complete the definition of a category, I should also describe when two morphisms $\Gamma \to \Delta$ are equal. There are actually many options here; the most strict is to say that they are equal only if the substitutions and proofs used are syntactically identical, and the most weak is to say that any parallel morphisms are equal. Neither of these is very useful; for purposes of this example, let us require only that the expressions substituted for each variable $X$ in $\Gamma$ can be proved equal in the context $\Delta$.

Now you should be able to prove that composition satisfies the axioms of a category.

Notice that the exact definition of equality of morphisms can depend heavily on the theory in question and your own purposes. For example, this definition makes sense only because we have a notion of proving equality of elements of a group. Also, you can sometimes place interesting conditions on whether two proofs count as equivalent, rather than requiring either syntactic identity or (as we do here) accepting proof irrelevance.

Exercise

Now that the category of contexts (in one sense) of the theory of a group has been completely defined, describe that category (up to equivalence) in terms familiar to an algebraist. In particular, compare it to the category of groups.

Answer

In rot13 (so that you have a chance to think about it yourself without accidentally seeing the answer): gur bccbfvgr bs gur pngrtbel bs svavgryl cerfragrq tebhcf.

The result of this exercise is true in more generality: it works for any finite-limit theory; see in particular Lawvere theory. Presumably there are also infinitary generalizations. There’s some general discussion in the Elephant.

Display morphisms

… display morphisms …

Related pages

• A way of describing categorical semantics, even for weak theories, which doesn’t require the explicit introduction of contexts is to use cartesian multicategories.

• The category of contexts is also known as the syntactic category of the corresponding theory.

References

Section D4.4 of

• Peter Johnstone, Sketches of an elephant,

A description of the construction of the category of contexts is in

• Andrew Pitts, Categorical logic, In Handbook of Logic in Computer Science, volume 5, pages 39–128. Oxford University Press (2001)

Another description, via sketches, is in chapter VIII of

• Paul Taylor, Practical Foundations of Mathematics,

A review of this is around section 2.8 of

• Paul Taylor, Foundations for computable topology (webpage)