🚀 go-pugleaf

In article <24458@alice.att.com> pereira@alice.att.com (Fernando Pereira)
 writes:

   >It cannot be characterized by any *finite* set of first-order formulas.

  Finiteness is not relevant here. It is a matter of what can be
expressed in first order logic. By compactness, any set of first order
formulas which has a model with the Herbrand universe
{0,s(0),s(s(0)),..} as its domain will have countable models
containing elements different from (the interpretations of) the terms
0,s(0), ec. Therefore it is not correct to say that adding the
(complete) first order identity theory of finite trees to the left of
|- is precisely restricting the class of models under consideration
from arbitrary first order models to finite tree models.  Similarly
for rational trees. Such a restriction cannot be achieved in first
order logic.