Pierce writes in his book in Def. 3.5.2 :
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.
So this means if a relation ( which is a set of term pairs, where the pairs are denoted as t->t' ) contains the element true->false
then that relation also satisfies the rules given in Fig. 3-1 because Def 3.5.2 does not forbid the presence of such elements in the relation which are not an instance of a conclusion of a rule.
So, in other words, the element true->false
is not an instance of the conclusion of E-IF, so the definition 3.5.2 does not tell anything about whether true->false
can be in a relation satisfying the rules in Fig 3-1 or not. Def 3.5.2 only talks about relation elements which have the form " if .... then .... -> .... "
, but does not explicitly forbid ( or actually say anything about ) the presence of the element true->false
, for example.
Question : is this understanding of mine correct ?
Yes, you are correct. A relation can satisfy the rules while also containing pairs that are not justified by the rules.
For example, if
R
is the evaluation relation presented in the text, which satisfies all of the rules in Fig. 3-1, then the relationR
plus your pairtrue -> false
also satisfies all of the rules. This makes sense since any relation must satisfy each rule in isolation; if we didn't allow additional pairs, then the relation{ if true then true else false -> true, if false then true else false -> false }
would not satisfy E-IfTrue in isolation since the second element cannot be justified by E-IfTrue. If the relation cannot satisfy that single rule in isolation, then it cannot satisfy all three of the rules presented. For this reason, additional "unjustifiable" pairs are allowed when satisfying an inference rule.That being said, the very next definition, 3.5.3, explicitly omits pairs like
true -> false
from the particular relation being discussed by specifying that it is the smallest relation satisfying all three rules. While we could discuss a larger relation, this restriction means that, in Pierce's words, "a statementt -> t'
is derivable iff it is justifiable by the rules."