# proof theory – Which context weakening rules are derivable in this system of equational logic?

I am trying to work through Andrew Pitts’ chapter on categorical logic: Categorical Logic. On page 7 he presents a system of equational logic. The rules are listed below:

$$dfrac{}{M = M : sigma (Gamma)}$$

$$dfrac{M = M^{prime} : sigma (Gamma)}{M^{prime}= M : sigma (Gamma)}$$

$$dfrac{M = M^{prime} : sigma (Gamma) quad M^{prime} = M^{prime prime} : sigma (Gamma) }{M = M^{prime prime} : sigma (Gamma)}$$

$$dfrac{M = M^{prime} : sigma (Gamma) quad N = N^{prime} : tau (Gamma,x: sigma, Gamma^{prime})}{N(M/x) = N^{prime}(M^{prime}/x): tau (Gamma,Gamma^{prime})}$$

Where for instance $$M : sigma (Gamma)$$ denotes that the term $$M$$ has sort $$sigma$$ and is given a context $$(Gamma)$$ which is a finite list of variable sort pairs which minimally include the variables occurring in the term $$M$$. Given the categorical semantics, it seems that if $$M = M^{prime} : sigma (Gamma)$$ is an equation in context, satisfied by a structure, then the structure should satisfy $$M = M^{prime} : sigma (Gamma^{prime prime})$$ where $$(Gamma^{prime prime})$$ is another context which contains $$(Gamma)$$ as a subsequence after possibly deleting some number of variable sort pairs. (I believe this because terms in context $$M : sigma (Gamma)$$ are interpreted as morphisms in a category with finite products and weakening of context corresponds to precomposition by a product of projection morphisms.)

However, on the syntactic side, I cannot seem to derive such a general form of weakening of the context of an equation. Given the rules for the system of equational logic I can only see how to derive the following less general context weakening rule:
$$dfrac{M = M^{prime} : sigma (Gamma) }{M = M^{prime} : sigma (Gamma,Gamma^{prime})}$$
from
$$dfrac{}{x = x : sigma (Gamma, x:sigma,Gamma^{prime})}$$
and
$$dfrac{M = M^{prime} : sigma (Gamma) quad x = x : sigma (Gamma,x: sigma,Gamma^{prime})}{M = M^{prime} : sigma (Gamma,Gamma^{prime})}$$

My question is: Is a more general context weakening rule derivable from the system or not? If not, should the system be extended to allow such a rule or is there a good reason not to have it?

Thank you very much for your consideration.

Posted on Categories Articles