Re: OWL 2 profiles

On 24 Nov 2010, at 04:33, Pat Hayes wrote:

> On Nov 23, 2010, at 8:06 PM, Bijan Parsia wrote:
> 
>> On 23 Nov 2010, at 19:08, Pat Hayes wrote:
>> 
>>> On Nov 23, 2010, at 11:46 AM, Cristian Cocos wrote:
[snip]
>> 
>> Not all RDF graphs under the standard semantics can be regarded as notation variants of classic (i.e., name separated) FOL formulae.
>> 
>> For example, ":a rdf:type :C" does not exactly correspond to C(a) (in a classic, introduction to symbolic logic style FOL).

I don't want to argue to much about things which don't matter. But I do think we should write to illuminate. In particular, a lot of people come from a textbook/GOFFOL background. In my experience, things like variable free syntax (a la DLs) or sorts (a la sorted logic) can be very confusing. So let's make such deviations clear.

> It corresponds exactly to the formula type(a, C) in a classic, textbook style FOL.

Or triple(a, rdf:type, C). Or...

The point is that it doesn't correspond to a monadic predicate application to a constant.

Now, ordinarily, one would think, "So what", but part of the meaning of the triple is that it *entails* something like:
	C(a)

By in large, in GOFFOL, C(a) is not entailed by ground formulae with binary predicates without auxilliary axioms.

Thus, on that translation, a rdf:type C is not a syntactic variant of any GOFFOL formula.

> It can be written as C(a) in a CL-style formulation of FOL, which is still strictly first-order. 

Yes, and obviously I've not disputed it, so you're picking on it is really quite otiose.

I think, in general, since the quite common view of FOL is that its strictly GOFFOL, that we should start our explanations on how OWL and RDF deviate from *that* while remain "first order logics" in the more general sense.

There's a big difference in ALC being a (notational variant of a) subset of GOFFOL, and RDF being a first order logic axiomatizable in a decidable set of GOFFOL, at least, in understanding what's going on.

>> However, it does not do so primarily via the reification *vocabulary*, but  via 1) some syntactic liberality (e.g., the signature is not sorted by syntactic role, but the set of  constants and predicates may overlap and, indeed, coincide)
> 
> Indeed, they can do so in a CL style FOL.

Yes, but, please, you have to admit that CL is not, in spite of the name, the most common FOL around. It's much more common to have a separated vocabulary. So start there.

> In fact, in CL there simply is no distinction between constants and predicates, or indeed functions and relations more generally; there is simply a set of names, and any name can play any syntactic role. This is not standard textbook FOL,

Yes! And when talking to people who are more likely to come from that background, it's helpful to presume that that is what they mean by "FOL".

> but it is still FOL, and indeed the standard FO inference rules apply to this syntax without change, and are still complete. 



>> and 2) additional semantic conditions.
> 
> There are no additional semantic conditions in CL. The CL model theory is an exact mirror of 'textbook' FOL

Wait for it!

> if one uses a syntax transcription which maps atomic sentences R(a1 ... an) to Apply(R a1 ... an). 

And, I presume some auxiliary axioms to recapture the the original meaning of the atomic sentences (or that the translation takes one formulae to *two*, i.e.,both R(a1...an) *and* Apply(R a1...an)).

Which is just a different *presentation* of addition semantic conditions.

>> However, at least through OWL Full, the particularly ways of doing this do not result in a logic which is e.g., non-compact. It, thus, may be completely defined in (classic, standard) FOL. Thus, it can be (and should be) regarded as a kind of first order logic even though it's not exactly classic, Principa style FOL.
> 
> There is a widely accepted criterion for being FO, according to which any logic which is compact and satisfies the downward Skolem-Lowenheim theorem is first order. 

Yes, as I indicated.

However, "being FO" is not generally "being FOL" where 'FOL' is used by a very wide linguistic community as a proper name for roughly GOFFOL/Textbook FOL, etc.

>> Note that the mere addition of comments can be regarded, reasonably, as a deviation from standard FOL.
> 
> I disagree about the reasonableness.

But that's silly. 

> There is no absolutely standard formulation of FOL:

If by "standard" you mean "standardized" then sure. If by "standard" you mean "having a strong lingusitic consensus" then *come on*. If you are writing a text book and you have a chapter with "FOL preliminaries" then you pretty much know what would be "standard" in such a formulation. 

> there are almost as many syntaxes as there are authors of textbooks.

There are almost as many *notations* as there are authors of textbooks (actually not, I'd say, by an order of magnitude).

But almost all (I believe) fall into a few abstract syntax patterns, e.g.,

Sentential connectives (~, &, v, ->, and <->) of which standardly you take some minimal subset for certain purposes.
Two quantifiers (some and all)
And a separated vocabulary of predicates (stratified by arity), functions (stratified by arity), and constants (though often regarded as 0-arity functions).

There's a set of standard variants (e.g., postfix or prefix; binary vs. nary &, v, etc.) But this is pretty damn standard.

> Adding comments does not affect the logic in any way, so to treat this as significant would be unreasonable. 

Of course they do. 1) they affect the syntax. 2) if you don't prune them from the abstract syntax tree in the parsing process, then you have to modify the interpretation function (at least implicitly).

This isn't a huge change, obviously, But subtle issues can arise and, historical, *have*.

[snip]
>> Anything that deviates from that slightly, but remains first order (in a general sense; e.g., can be axiomitized by a finite GOFFOL theory with maybe some axiom schemas) is "New Fangled FOL" or NFFOL. RDF is definitely a NFFOL
> 
> I disagree. It depends on how to transcribe the RDF into the logical notation. If you do it uniformly so that each triple a P b is rendered into the formula 
> triple (a P b), then you get GOFOL.

As I pointed out above, there are differences such as the signatures and the set of validities. Since it's reasonable to define a logic by the set of validities, then I think a difference in that set indicates a deviation from that logic.

> If you treat properties as binary relations and classes as predicates, you get a CL-style syntax. But that difference is superficial: nothing in RDF requires inferences going beyond classical FO inference.

Sure it does. You need at least the axiomatic triples. Those do not appear in the set of validities for GOFFOL, or for most FOLs.

> In fact, its a very small subset of FO inference. In fact, this applies to RDFS and all the OWLs also. 

It's not quite that you're wrong per se, in that I can add a bunch of background assumptions that makes what you're saying fine. I generally understand you. But I have to explain quite a bit to make this claim work to people who don't share those assumptions. Those assumptions aren't common. You asserting that they are common really doesn't make it so. Of course, my asserting that they don't doesn't either, but I'd be happy for us to go to a library and pull down symbolic logic texts and check some of these.

> BTW, you can think of the CL version of FOL as being a first-order GOFOL theory which has a signature but no axioms.

Oookay. 

> It is an empty theory, which serves only to achieve a syntactic transformation.

Uh...this doesn't make any sense. How does an empty theory "achieve" a syntactic transformation?!

> That is why the inference rules apply without any change. 

I would imagine that there is a translation from CL to GOFFOL such that the translated theory entails a certain class of formulae iff the CL theory entails the corresponding formulae. But I'm pretty sure that the translated theory is going to have a different non-trivial axiom count :)
[snip]
>>> There is no reification 'mechanism' in RDF, and the RDF semantics of reification are so minimal as to pose no threat to FO expressivity. 
>> 
>> It's NFFOL but not GOFFOL.
> 
> The real point is, its FOL. 

Actually, the real point (I suspect) for Cristian was what I wrote below about the difference. :)

But yet again a megaemail. Probably not useful, but I hope against hope.

Cheers,
Bijan.

Received on Wednesday, 24 November 2010 05:39:07 UTC