second-order aint reflection

From: pat hayes (
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 
authority of your collective imprimateur.

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?


Pat Hayes
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax

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