2
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ 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 $\endgroup$ – rindPHI Jul 20 '14 at 7:55
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Martin Berger Apr 11 at 11:47
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Apr 11 at 12:12
  • $\begingroup$ 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 ... ? $\endgroup$ – Martin Berger Apr 11 at 12:29
  • $\begingroup$ 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? $\endgroup$ – Andrej Bauer Apr 11 at 15:34
  • $\begingroup$ Rules are foundationally prior to closure operators. The latter are an ex-post rationalisation of the former. $\endgroup$ – Martin Berger Apr 12 at 9:02
-1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Apr 11 at 10:47
  • 1
    $\begingroup$ @AndrejBauer, I believe he meant the OP's stackexchange question, for which the statement seems true. $\endgroup$ – Andreas Rossberg Apr 12 at 3:01
  • $\begingroup$ @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. $\endgroup$ – Andrej Bauer Apr 13 at 10:09
  • $\begingroup$ @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 $\endgroup$ – Matteo Apr 13 at 11:54
  • $\begingroup$ Ah! Sorry for being dense. $\endgroup$ – Andrej Bauer Apr 13 at 15:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.