TAPL: Explanation and example(s) for satisfied

This question arises from my reading of "Types and Programming Languages" (WorldCat) by Benjamin C. Pierce.

On page 36 is the definition for satisfied


A rule is satisfied by a relation if, for each instance of the rule,
either the conclusion is in the relation or one of the premises is
not.

On page 36 is the definition for instance


An instance of an inference rule is obtained by consistently replacing
each metavariable by the same term in the rule's conclusion and all its
premises (if any).


For example


if true then true else (if false then false else false) -> true


is an instance of E-IFTRUE, where both occurrences of $t_2$ have been
replaced by true and $t_3$ has been replaced by if false then false else
false.

On page 15 is the definition for relataion


An n-place relation on a collection of sets $S_1, S_2,..., S_n$ is a
set $R\subseteq S_1\times\;S_2\;\times\;...\;\times\;S_n$ of tuples
of elements from $S_1$ through $S_n$. We say that the elements $s_1\in
> S_1$ thorugh $s_n\in S_n$ are related by $R$ if $(s_1,...,s_n)$ is an
element or $R$.

On page 36 is the definition for one-step evaluation relation ($\rightarrow $)


The one-step evaluation relation $\rightarrow $ is the smallest
binary relation on terms satisfying the three rules of Figure 3-1.
When the pair $(t,t')$ is in the evaluation relation, we say that "the
evaluation statement (or judgment) $t \rightarrow t'$ is derivable."

On page 34 are the three rules from Figure 3-1

E-IFTRUE


\begin{equation}if\;true\;then\;t_2\;else\;t_3\;\rightarrow\;t_2\end{equation}

E-IFFALSE


\begin{equation}if\;false\;then\;t_2\;else\;t_3\;\rightarrow\;t_2\end{equation}

E-IF


\begin{equation}\frac{t_1\rightarrow\;t_1'}{if\;t_1\;then\;t_2\;else\;t_3\;\rightarrow\;if\;t_1'\;then\;t_2\;else\;t_3}\end{equation}

Can someone explain this definition and give an example for parts of the defintion.

1. The conclusion is in the relation.

1. One of th

One way of reading the definition of satisfied that might help is to change


A rule is satisfied by a relation if, for each instance of the rule, either the conclusion is in the relation or one of the premises is not.

to the logically equivalent statement


A rule is satisfied by a relation if, for each instance of the rule, if all the premises are in the relation, then the conclusion is in the relation.

Thus if the rule says, for instance,

$$
\dfrac{A \to B \quad B\to C}
{A\to C}
$$

Then binary relation $R$ satisfies this rule whenever for each instance of the rule, such as

$$
\dfrac{a \to b \quad b\to c}
{a\to c}
$$

if $(a,b)\in R$ and $(b,c)\in R$, then $(a,c)\in R$.

Another way of stating this is that $R$ is closed by the rule (though this probably doesn't make it clearer).

Now let's return to the original statement. What


A rule is satisfied by a relation if, for each instance of the rule, either the conclusion is in the relation or one of the premises is not.

is saying is that is it okay to have $(a,c)$ in the relation without the premises, but if all of the premises are in the relation, then $(a,c)$ must be. That is, it is okay to have not all of the premises in the relation, without imposing any additional constraint.

Personally, I think that thinking about this definition in terms of an implication is simpler, so I help this explanation helps.

StackExchange Computer Science Q#10386, answer score: 7