<p>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.</p>

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

<p>There is only one judgement form <span class="math-container">$\vdash A$</span> and only two judgement rules
<span class="math-container">$$
\frac{ }{\vdash \top}
\qquad
\frac{\vdash A \qquad \vdash B}{\vdash A \land B}
$$</span>
It should be clear that <span class="math-container">$\vdash A$</span> is derivable if, and only if, <span class="math-container">$A$</span> is an expression which contains no <span class="math-container">$\bot$</span>'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.</p>

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

<p>Suppose we place a side condition <span class="math-container">$\phi$</span> on the second rule:
<span class="math-container">$$
\frac{ }{\vdash \top}
\qquad
\frac{\vdash A \qquad \vdash B}{\vdash A \land B} \ \text{if $\phi(A,B)$}
$$</span>
Here <span class="math-container">$\phi$</span> can be any condition on the expressions. For instance, it could be <span class="math-container">$A \neq B$</span> (but in that case there will be a better way of writing the rule without a side condition), or perhaps it says that <span class="math-container">$A$</span> has fewer occurrences of <span class="math-container">$\bot$</span> than <span class="math-container">$B$</span>, or whatever. The side condition limits the family of closure rules determined by the rule:
<span class="math-container">$$\mathscr{C} = \{(\emptyset, \top)\} \cup \{(\{A,B\},A \land B) \mid A, B \in \mathscr{E} \ \text{and}\ \phi(A,B)\}.$$</span>
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.</p>

<p>In the example of the variable rule that you mention,
<span class="math-container">$$\frac{ }{\Gamma \vdash x : T} \ \text{if $(x:T) \in \Gamma$},$$</span>
we clearly have a side-condition.</p>

<p>It is called a <em>side</em>-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.</p>

CC BY-SA 4.0
2019-04-11T11:47:21.380Z
I habitually write all premisses including side conditions
above the line making them look like normal premises. Primarily because that
is:
(1) More uniform.
(2) Easier to typeset.
(3) Easier to read.

_A paper is no HOL proof script._  In case any what to put in meta and
what to put on the object level is a bit arbitrary, is mostly a question of
convenience anyway, and one could rewrite the rule system so the
side-conditions move from meta to object level.
Martin Berger
CC BY-SA 4.0
2019-04-11T12:12:03.190Z
It may be a rather non-trivial level to stuff side-conditions into the object-level. Sure, you can always introduce another judgement form to handle the side condition.
Andrej Bauer
CC BY-SA 4.0
2019-04-11T12:29:15.980Z
Agreed, it might be highly non-trivial, e.g. free vs bound vs fresh names. One could argue this is not even fully solved. That problem doesn't go away by writing side conditions on the side. Aside: what if you have more than 2 rule systems / meta-levels involved ... ?
Martin Berger
CC BY-SA 4.0
2019-04-11T15:34:36.717Z
As long as we keep in mind the fact that the rules are just a rather simple way of specifying a closure operator, we shouldn't think they're necessary or special. They're just convenient in many cases that logic considers. But as soon as they become an obstacle, why stick to them?
Andrej Bauer
CC BY-SA 4.0
2019-04-12T09:02:24.260Z
Rules are foundationally prior to closure operators. The latter are an ex-post rationalisation of the former.
Martin Berger
CC BY-SA 4.0
2019-04-12T18:06:14.553Z
Only if you think that logic is prior to mathematics.
Andrej Bauer
CC BY-SA 4.0
2019-04-13T10:00:55.300Z
I'm not sure if you are familiar with [this book](https://homotopytypetheory.org/book/) but it takes rules as given ... Be that as it may, this is not the right place to discuss foundations of mathematics and their relations to natural language.
Martin Berger
CC BY-SA 4.0
2019-04-13T10:07:35.570Z
Yeah, I've heard to book is ok.
Andrej Bauer
CC BY-SA 4.0
2019-04-11T10:37:04.687Z
2019-04-11T10:42:06.430Z
2019-04-11T10:42:06.430Z
Andrej Bauer
<p>This is a rather interesting matter and the question has long been left unanswered, so I'll attempt an answer myself.</p>

<p>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 <span class="math-container">$\in$</span>, that is most certainly not included in the language we are considering, nor in the deduction system.</p>

<p>Note that there is a very simple way to express this rule without the need of any side condition:
<span class="math-container">$$ \frac{}{\Gamma, x: T \vdash x : T} $$</span>
I personally find this more satisfactory.</p>

<p>The matter can get more sophisticated: consider the <span class="math-container">$\forall$</span>-left rule of Gentzen's sequent calculus LK
<span class="math-container">$$ \frac{\Gamma \vdash \varphi}{\Gamma \vdash \forall x.\varphi} (x \text{ not free in }\Gamma)$$</span>
Here the condition plays a more important role, and indeed the rule is stated like this in most expositions (it is the famous <em>eigenvariable</em> 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 <span class="math-container">$\Gamma$</span>:
<span class="math-container">$$ \frac{\Xi,x;\Gamma \vdash \varphi}{\Xi;\Gamma \vdash \forall x.\varphi}$$</span>
In this subtler case one might argue that we are expressing a precise philosophical stance: that is, there is no such thing as a <em>free variable</em>, but rather one should specify an "interface" to a proof/program, that allows it to interact with external specifications.</p>

CC BY-SA 4.0
2019-04-11T10:47:51.227Z
What is your basis for the statement that the the question "has long been left unanswered"? A decent textbook on logic will answer this question.
Andrej Bauer
CC BY-SA 4.0
2019-04-12T03:01:34.493Z
@AndrejBauer, I believe he meant the OP's stackexchange question, for which the statement seems true.
Andreas Rossberg
CC BY-SA 4.0
2019-04-13T10:09:29.053Z
@AndreasRossberg: I am not sure I am following you. In any case, this question and the subject matter are very standard and well understood. There is no mystery.
Andrej Bauer
CC BY-SA 4.0
2019-04-13T11:54:29.787Z
@AndrejBauer Andreas correctly notices that the basis for my statement is that OP had asked the question on Jul 19 '14 and had not received an answer so far
Matteo
CC BY-SA 4.0
2019-04-13T15:44:22.147Z
Ah! Sorry for being dense.
Andrej Bauer
CC BY-SA 4.0
2019-04-10T13:27:39.100Z
2019-04-10T13:27:39.100Z
Matteo
<p>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?</p>

<p>$Update$:</p>

<p>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.</p>

<p>$Update^2$:</p>

<p>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 <em>aside</em>, leaving the premises empty to indicate that it is an axiom, though conditional:</p>

<p>$$\frac{}{\Gamma \vdash x : T} (x : T) \in \Gamma$$</p>

<p>while in others, it is put <em>above</em> as if it were a premise:</p>

<p>$$\frac{(x : T) \in \Gamma}{\Gamma \vdash x : T}$$</p>

CC BY-SA 3.0
2014-07-20T07:55:18.127Z
Since I do not have enough reputation to comment in this stackexchange variant, I have to post this question to yours as an answer: Could you please give an example to such a "side condition"? I'm not quite sure that I actually get your point. *Update:* Thanks, the example makes it clearer. As long as there are no other examples for this notation, I am quite sure that putting these conditions, which obviously do not belong to the language of the calculus, on the top of axioms, is just syntactic sugar for saving space or for stressing the point that the application of the axiom is justified at
rindPHI
<lo.logic><type-theory><proof-theory>
About the position of side conditions in an inference rule
day
# About the position of side conditions in an inference rule

(Asked by: username_0 on 2014-07-19)

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}$$

**Tags:** lo.logic, type-theory, proof-theory
> **Comments:**
> **username_1**: Since I do not have enough reputation to comment in this stackexchange variant, I have to post this question to yours as an answer: Could you please give an example to such a "side condition"? I'm not quite sure that I actually get your point. *Update:* Thanks, the example makes it clearer. As long as there are no other examples for this notation, I am quite sure that putting these conditions, which obviously do not belong to the language of the calculus, on the top of axioms, is just syntactic sugar for saving space or for stressing the point that the application of the axiom is justified at  

---

## 2 answers

### Answer by username_2 on 2019-04-11. Score: 3

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.

> **Comments:**
> **username_3**: I habitually write all premisses including side conditions above the line making them look like normal premises. Primarily because that is: (1) More uniform. (2) Easier to typeset. (3) Easier to read.  _A paper is no HOL proof script._  In case any what to put in meta and what to put on the object level is a bit arbitrary, is mostly a question of convenience anyway, and one could rewrite the rule system so the side-conditions move from meta to object level.  
> **username_2**: It may be a rather non-trivial level to stuff side-conditions into the object-level. Sure, you can always introduce another judgement form to handle the side condition.  
> **username_3**: Agreed, it might be highly non-trivial, e.g. free vs bound vs fresh names. One could argue this is not even fully solved. That problem doesn't go away by writing side conditions on the side. Aside: what if you have more than 2 rule systems / meta-levels involved ... ?  
> **username_2**: As long as we keep in mind the fact that the rules are just a rather simple way of specifying a closure operator, we shouldn't think they're necessary or special. They're just convenient in many cases that logic considers. But as soon as they become an obstacle, why stick to them?  
> **username_3**: Rules are foundationally prior to closure operators. The latter are an ex-post rationalisation of the former.  
> **username_2**: Only if you think that logic is prior to mathematics.  
> **username_3**: I'm not sure if you are familiar with [this book](https://homotopytypetheory.org/book/) but it takes rules as given ... Be that as it may, this is not the right place to discuss foundations of mathematics and their relations to natural language.  
> **username_2**: Yeah, I've heard to book is ok.  

---

### Answer by username_4 on 2019-04-10. Score: -1

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.

> **Comments:**
> **username_2**: What is your basis for the statement that the the question "has long been left unanswered"? A decent textbook on logic will answer this question.  
> **username_5**: @AndrejBauer, I believe he meant the OP's stackexchange question, for which the statement seems true.  
> **username_2**: @AndreasRossberg: I am not sure I am following you. In any case, this question and the subject matter are very standard and well understood. There is no mystery.  
> **username_4**: @AndrejBauer Andreas correctly notices that the basis for my statement is that OP had asked the question on Jul 19 '14 and had not received an answer so far  
> **username_2**: Ah! Sorry for being dense.  

---

