Re: second-order aint reflection

From: Ian Horrocks (
Date: 10/11/00


Thanks for pointing this out. I agree that this section should be

Regards, Ian

On October 10, pat hayes writes:
> 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?
> Thanks.
> 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