About the position of side conditions in an inference rule

Question

Sometimes I see people put side conditions above the inference line as if they were premises of an inference rule. This feels strange. My understanding (which may be wrong) is that a side condition belongs to the meta-theory, not to the object-theory: an object-proof of a side condition should not be required and may even not be possible. So what is the motivation of doing this? For saving space or for some other deeper reason?

$Update$:

I am no longer quite sure whether a side condition belongs to the meta-theory. But at least it is outside the object-theory the inference rules describe,that is, the truth of a side condition cannot be derived using the inference rules.

$Update^2$:

Take as an example the rule for typing variables from the simply-typed $\lambda$-calculus. $(x : T) \in \Gamma$ is a side condition that tests whether the variable $x$ of type $T$ is in the typing context $\Gamma$. In some presentations, the side condition is put aside, leaving the premises empty to indicate that it is an axiom, though conditional:

$$\frac{}{\Gamma \vdash x : T} (x : T) \in \Gamma$$

while in others, it is put above as if it were a premise:

$$\frac{(x : T) \in \Gamma}{\Gamma \vdash x : T}$$

Answer 1

An inference rule is a symbolic representation of an entire family of closure rules. A side condition cuts down such a family to a subfamily. It is perhaps best to show an example.

We consider the following toy variant of the propositional calculus. The language of expressions is built from primitive constants $\top$ and $\bot$, and a binary connective $\land$. Let $\mathscr{E}$ be the set of all expressions we can build in this language (they correspond to binary trees whose leaves are labeled with $\bot$ and $\top$).

There is only one judgement form $\vdash A$ and only two judgement rules $$ \frac{ }{\vdash \top} \qquad \frac{\vdash A \qquad \vdash B}{\vdash A \land B} $$ It should be clear that $\vdash A$ is derivable if, and only if, $A$ is an expression which contains no $\bot$'s. Now, how precisely do we read the above inference rules? Bare with me while I describe closure rules and closure operators. These provide an order-theoretic explanation of what rules of inference are and what derivability is about.

Each rule determines a family of closure rules. A closure rule is a pair $(S, A)$ where $S \subseteq \mathscr{E}$ and $A \in \mathscr{E}$. In our case we get the following family of closure rules $\mathscr{C}$: $$\mathscr{C} = \{(\emptyset, \top)\} \cup \{(\{A,B\},A \land B) \mid A, B \in \mathscr{E}\}$$ Such a family then induces a closure operator $F_\mathscr{C} : P(\mathscr{E}) \to P(\mathscr{E})$ on the powerset of expressions, defined by $$F_\mathscr{C}(X) = \{A \mid \exists S \subseteq X . (S, A) \in \mathscr{C}\}.$$ The set of all derivable judgements is precisely the least fixed point of $F_\mathscr{C}$. The least fixed point exists by Tarski's theorem because $F_\mathscr{C}$ is a monotone operator on a complete lattice.

Suppose we place a side condition $\phi$ on the second rule: $$ \frac{ }{\vdash \top} \qquad \frac{\vdash A \qquad \vdash B}{\vdash A \land B} \ \text{if $\phi(A,B)$} $$ Here $\phi$ can be any condition on the expressions. For instance, it could be $A \neq B$ (but in that case there will be a better way of writing the rule without a side condition), or perhaps it says that $A$ has fewer occurrences of $\bot$ than $B$, or whatever. The side condition limits the family of closure rules determined by the rule: $$\mathscr{C} = \{(\emptyset, \top)\} \cup \{(\{A,B\},A \land B) \mid A, B \in \mathscr{E} \ \text{and}\ \phi(A,B)\}.$$ Thus we see that the side-condition lives at the "meta-level", because it does not appear inside the closure rules, but instead gives an additional condition on the closure rules themselves.

In the example of the variable rule that you mention, $$\frac{ }{\Gamma \vdash x : T} \ \text{if $(x:T) \in \Gamma$},$$ we clearly have a side-condition.

It is called a side-condition because it is written on the side. And it is so written for a reason, namely to make it clear that it is not a premise of the rule. This is especially important when the object-language described by the rule uses the same symbols as the meta-level language and confusion could ensue. However, it has become fashionable in certain circles to write side-conditions above the line. I am not sure it is a good idea to write side-conditions above the line, as it confuses students and newcomers, but it is stylistically a bit more pleasing.

Answer 2

This is a rather interesting matter and the question has long been left unanswered, so I'll attempt an answer myself.

As the comment points out, the difference among the two formats proposed in the second update seems to just be syntactic sugar. However I find the second one, if possible, even more misleading: indeed, it places in the premise the symbol $\in$, that is most certainly not included in the language we are considering, nor in the deduction system.

Note that there is a very simple way to express this rule without the need of any side condition: $$ \frac{}{\Gamma, x: T \vdash x : T} $$ I personally find this more satisfactory.

The matter can get more sophisticated: consider the $\forall$-left rule of Gentzen's sequent calculus LK $$ \frac{\Gamma \vdash \varphi}{\Gamma \vdash \forall x.\varphi} (x \text{ not free in }\Gamma)$$ Here the condition plays a more important role, and indeed the rule is stated like this in most expositions (it is the famous eigenvariable condition). Even here one has the opportunity to not mention an external condition by means of extra care, if one creates a new environment to keep track of the eigenvariables and make sure that they dont leak into $\Gamma$: $$ \frac{\Xi,x;\Gamma \vdash \varphi}{\Xi;\Gamma \vdash \forall x.\varphi}$$ In this subtler case one might argue that we are expressing a precise philosophical stance: that is, there is no such thing as a free variable, but rather one should specify an "interface" to a proof/program, that allows it to interact with external specifications.