About the position of side conditions in an inference rule 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}$$
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.