Re: SEM: "natural" entailments

>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.

>
>>   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.

>
>>  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.

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.)  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 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) ).

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 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. And as a result we are trapped in all kinds of arcane 
technical debates which are completely irrelevant to almost everyone, 
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 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 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 14:59:35 UTC