From: Ian Horrocks (horrocks@cs.man.ac.uk)
Date: 10/11/00
Pat, Thanks for pointing this out. I agree that this section should be clarified/corrected. 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 > phayes@ai.uwf.edu > http://www.coginst.uwf.edu/~phayes
This archive was generated by hypermail 2.1.4 : 03/26/03 EST