# second-order aint reflection

From: pat hayes (phayes@ai.uwf.edu)
Date: 10/10/00

```Greetings, authors of "An informal description of OIL...". Thanks for
writing this very readable paper, but you make one serious error in
the discussion towards the end, under the heading "heavy oil", when
you identify second-order expressivity with reification. These are
not the same thing, and it would be a pity to have this widespread
confusion made even worse by its being given the considerable

Second-order refers to a language which can quantify over properties
and relations as well as the individuals to which those properties
and relations apply. Reification refers to the ability of a langauge
to describe its own syntax, ie as you correctly observe, with
"statements of the language as objects". But statements are not the
same kind of thing as properties and relations, and it is important
to keep these distinctions clear. For example, you say that
unification is undecideable in second-order logic. This is true in a
second-order logic where the quantification over predicates and
relations is understood to range over all mathematically expressible
relations; the reason is that such a unification must allow for
arbitrary amounts of lambda-conversion.  But the second-order
quantifiers can be understood in other ways. If the quantifiers are
understood to range over all mathematically possible relations, then
theorem-hood is not even recursively enumerable, so no complete logic
is possible; on the other hand, if it can be understood to range over
only relations which are named in the language, then first-order
unification is complete. But, to emphasise my main point, none of
this interpretive variation is possible for reification, since the
meaning of a quantifier ranging over all *expressions* is fixed by
the syntax of the langauge itself.  Reification in itself does not
require any kind of higher-order construction; after all, syntax
consists of tree structures (there are some technical issues here, I
know, if one wants the trees to be finite.) . But reification brings
its own problems which are quite different; notably, being too
generous with reification allows the language to become paradoxical,
which is widely thought of as an undesirable trait in a logic. There
is nothing paradoxical in second-order logic.

This confusion may have arisen from the observation that what makes
second-order unification difficult is lambda-conversion, and one can
think of lambda-conversion as an operation on expressions. But it is
important to keep clear the difference between an expression, on the
one hand, and the relation or function denoted by that expression, on
the other. Putting the latter into the semantics might force the
former into the syntax, but putting the former into the semantics
gets one into a completely different kettle of fish.

Since there is such a wide interest in 'web logic', and since so much
of this interest is from people without a deep technical background
in logic, I wonder if I could urge you to revise your paper to
correct this misleading and potentially confusing remark?

Thanks.

Pat Hayes
---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes
```

This archive was generated by hypermail 2.1.4 : 03/26/03 EST