# Re: second-order aint reflection

From: Ian Horrocks ([email protected])
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
> [email protected]
> http://www.coginst.uwf.edu/~phayes
```

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