Re: SEM: "natural" entailments

On September 24, pat hayes writes:
> 
> >On September 17, pat hayes writes:
> >
> >[snip]
> >
> >>  >Finally, I would like to point out (again) that DLs are nothing more
> >>  >than decidable subsets of FOL with useful computational
> >>  >properties.
> >>
> >>  You keep saying this, but that isn't the impression I get. For
> >>  example, the recent DQL document has to have a footnote pointing out
> >>  that DAML doesn't have any notion of 'conjunction', strictly
> >>  speaking.
> >
> >It doesn't say that, it says that "DAML+OIL does not have a logical
> >connective for conjoining sentences or for conjoining knowledge
> >bases". It is simply the case that in DAML+OIL the use of the
> >conjunctive connective is not defined for sentences or KBs (it would
> >be easy to add such a definition). The lack of such a definition
> >doesn't stop the language from being (isomorphic with) a SUBSET of
> >FOL.
> 
> Without conjunction, it must be a pretty trivial subset. That rules 
> out all the binary connectives.
> 
> >
> >>   So the inference
> >>
> >>  A, B |= (A and B)
> >>
> >>  which is about the simplest inference imaginable, so simple that
> >>  Aristotle didn't bother to give it a name, apparently isn't supported
> >>  by DLs.
> >
> >In a DL there are some syntactic restrictions on the form of A and B:
> >recall that it is a SUBSET of FOL and not full FOL. If A and B are
> >classes (i.e., formulae with one free variable), then there is no
> >problem:
> >
> >A(x),B(x) |= (A and B)(x)
> >
> >for all A, B and x.
> 
> ?? That isn't a valid FOL inference. Its not even *well-formed* in 
> FOL. The nearest FOL expression that I can think of (and its only FO 
> if you allow a free-wheeling KIF style of syntax) is:
> 
> A(x), B(x) |= (exists (C) (forall (y) (iff C(y) (and A(y) B(y) )))), C(x)
> 
> which is also not FOL valid, but it might be a reasonable axiom in a 
> simple theory of predicates/sets.

I didn't bother to do the standard syntactic translation of a class
(e.g., A and B) into a formula with one free variable. This produces
A(x) ^ B(x). So the whole thing becomes:

A(x),B(x) |= A(x) ^ B(x)


> >>   And the 'strong' OWL semantics requires us to assert (or
> >>  assume) that the class (union A B) must *exist* in order to validate
> >>  the DL version of the inference
> >>
> >>  A |= (A or B).
> >
> >again, it does:
> >
> >A(x) |= (A or B)(x)
> 
> That is not the inference I cited. The difference is instructive, in 
> fact: I cited an elementary principle of propositional reasoning, one 
> that is incorporated into all human languages and probably into most 
> human thought processes; and in return you cited a special  case of a 
> set-theoretic comprehension axiom which is not first-order valid.

Again, with the standard expansion we get:

A(x) |= A(x) v B(x)


> 
> >
> >>  That sure doesn't feel like a subset of FOL to me; it feels a lot
> >>  more like a subset of ZF set theory. Those inferences are valid in
> >>  propositional logic where there aren't any classes to exist in the
> >>  first place. Union and intersection are *analogous* to disjunction
> >>  and conjunction, but they are not the *same*.
> >
> >This is getting silly.
> 
> I don't agree, I think it is central.
> 
> >The correspondence between Description/modal
> >logics and *standard* FOL is very well know, e.g., see [1] for an
> >overview and relevant results dating back to the 1960s.
> 
> I know about the *correspondence*.
> 
> >I don't want
> >to get into a philosophical argument about what it means to be the
> >"same". For me it is enough to point out that DLs and their
> >corresponding fragment of FOL have models that are completely
> >isomorphic.
> 
> Well, sorry, but this 'philosophical argument' (interesting that you 
> use 'philosophical' as a dismissive; its a revealing rhetorical 
> device often used by engineers) is central to what we are trying to 
> do here. Its not just about isomorphic models. At the very least, we 
> should be paying some closer attention to proof theory; but more 
> centrally, the ways of thinking embodied in these logical frameworks 
> need to be taken seriously. The entire game is to develop a 'web 
> logic' that will enable people to mark up their websites with 
> intuitively reasonable information expressed in a machine-useable 
> form. These people are not going to have read [1] and are not going 
> to find it natural to be forced to fit their thinking into a 
> straightjacketed form, even if it is mathematically isomorphic to a 
> more natural one; particularly if that form requires them to adopt a 
> 'philosophical' (it would be more accurate to say 'ontological') 
> framework for thinking that runs counter to the one they actually 
> think with. For example, the idea that one should only be allowed to 
> conclude A and B from B and A  under restricted circumstances, and 
> that this can only be done by concluding that new predicates exist 
> is, frankly, ridiculous.

That would be ridiculous, but no one is suggesting it (well I'm not
anyway).


> The DL framework forces us all - lay users and us techies - into 
> thinking about the existence of classes all the time. And that is not 
> a natural way to think, for many purposes. (For some,  but not for 
> all.)  

I agree that not everyone finds class based languages natural. If you
prefer, you can simply write in the relevant subset of FOL and
translate that into OWL.

> Just look, for example, at the extraordinary lengths that 
> Peter and I have been driven by the need to justify these silly 
> 'closure' conditions on the OWL universe. I say silly because if the 
> actual logical content of OWL were all written out straightforwardly 
> in sentential form, the existence of the relevant domains would be a 
> trivial consequence of Herbrand's theorem; the issue would not even 
> arise. And yet, not only does it arise, purely as an artifact of the 
> warped semantic framework of DLs, but it is seen as central, a 
> stumbling block to progress and a huge obstacle to comprehension by 
> implementers and users.

It is nothing to do with DLs. It is an artifact of the requirement to
have RDF entailment be coincident with OWL entailment. The same
problem would arise with any other fragment of standard FOL.

> It is a very bad sign, for example, that 
> Russell's paradox even became a topic of conversation in Webont, let 
> alone a topic that has diverted our best efforts for over 9 months. 
> The logicians had that one settled in about 1930, before Tarsky even 
> invented model theory. It just should never have come up. It only did 
> because some people apparently think that saying (A and B) involves 
> creating a class (lambda x. (A and B)(x) ).

Again, this problem is entirely the result of trying to embed a subset
of standard FOL into a non-standard logical framework like RDF. If RDF
were a fragment of standard FOL in the same sense that DLs are, i.e.,
just a syntactic variant, then the problem would not arise.


> You are always emphasizing the fact that we cannot afford to indulge 
> in original research work: we must stick to the standards. But when 
> it comes to the basic framework of the languages, the standard were 
> worked out over 50 years ago, and yet you insist on rejecting this 
> well-understood framework and dragging us into this swamp of closure 
> conditions, comprehension principles, recursive domains and fussy 
> limitations on expressivity. Sorry, Ian, but you are wrong. DL's may 
> be *isomorphic* to a subset of FOL, via a curious mapping (Im not 
> even fully persuaded of this, by the way: are DL's always compact, 
> for example? They refer to integers in their semantic conditions, 
> which is slightly worrying) but they are definitely not a subset of 
> FOL; and their syntax , metatheory and semantics are all quite unlike 
> FOL. Most of OWL is not even FOL logically valid.  FOL semantics does 
> not support any inference to the existence of an un-named predicate.

I like original research as much as the next guy, but I still maintain
that it is crazy to be basing standards on it as you go, before the
results have even been subjected to extended scrutiny and review - and
by extended scrutiny and review I mean something more than Peter
looked at it for a few days/weeks and didn't find any glaring
inconsistencies (sorry Peter).

Basing the language on existing frameworks is exactly what I want to
do - I want to base it on a decidable subset of standard FOL. If you
disagree with the very large body of work showing that DLs are simply
a notational variant of such a subset, then I suggest that you get
writing - you will certainly be able to get some major publications
out of it. The mapping/correspondence is quite trivial - you can write
it down on the back of a postcard. Whether you consider it to be
curious is obviously subjective. DLs do not support "inference to the
existence of an un-named predicate" either - I don't know where you
get this idea from. You seem to be confusing the underlying language
with attempts to embed it in RDF.


> >I must say that I just don't understand what your problem is with
> >this.
> 
> My problem, which has been present since I first got involved with 
> DAML but which I have largely kept quiet about in the interests of 
> making progress, not rocking the boat, etc.., is that the entire SW 
> effort is being driven along a path which I am increasingly convinced 
> is the wrong path for it to be on. It has been hijacked by the 
> description logicians, and the anti-logic fuzzies have let this 
> happen because both of them can agree over a drink that, whatever 
> else may separate them, neither of them would ever want Webont to be 
> an actual *logic*. (Heavens to Betsy, what a terrible idea!) And the 
> result has been that Webont is now in a blind alley, trying to 
> persuade the entire planet to adopt a notation which is at odds with 
> about a century of clear understanding of meanings, proofs and 
> connections to thought and language, all of which has been tossed 
> aside.

What are we meant to be tossing aside? As I keep saying, I want to
use stuff that is well established ant that builds on a great history
of existing work - not something we lashed up last week.

> And as a result we are trapped in all kinds of arcane 
> technical debates which are completely irrelevant to almost everyone, 

Again, this is an artifact of attempts to embed the language in RDF.


> and tiptoeing nervously around issues which we should be able to 
> settle in an afternoon and implement in a couple of weeks ( like how 
> to incorporate "rules", by which people mean simple implications. Use 
> Horn clauses, do backtracking with an efficient unification 
> algorithm, OK? End of story, for God's sake. Stefan implemented it 
> already months ago. Lets get on with something more interesting and 
> useful.)  My experience with trying to make sense of OWL has left me 
> with the overwhelming feeling that this whole DL framework has now 
> become more of a burden than it is worth. And it is, to make the 
> point once more, NOT a subset of FOL. That claim is literally false 
> and (IMO) highly misleading.

It is a notational variant of a subset of FOL. This is very well
established. 


> It is a subset of a first-order set 
> theory; and it is centrally concerned, like all set theories, with 
> the complex and subtle ways in which its comprehension principles 
> interact, and the need to provide just enough sets but not too many. 

This is completely wrong. There is no question of comprehension
principles or providing just enough sets. All I am doing is writing
down FOL using what you deem to be a funny notation (but I like
it). When I write down C subClassOf D, feel free to think of this as
forall x . C(x) -> D(x). There is a well known (and pretty obvious)
way in which the various class constructors can be recursively
decomposed so that all classes become formulae with one free
variable. E.g., Restriction (onProperty P allValuesFrom C) becomes
(forall y . P(x,y) -> C(y)). So, when I write down such a restriction
you can just think of it as funny syntax for the FOL. The advantage of
the funny notation is that it neatly defines some interesting
decidable subsets of FOL. That is all there is to it.

Ian

> This is a fascinating topic in foundations of mathematics, but (1) we 
> are all of us amateurs at it, and (2) it seems totally irrelevant to 
> the SW. We would be better spending our time helping Tim get N3 
> sorted out.
> 
> Pat
> 
> 
> -- 
> ---------------------------------------------------------------------
> 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

Received on Tuesday, 24 September 2002 19:04:09 UTC