Re: class and inviduals

On 19 Nov 2010, at 00:13, Pat Hayes wrote:

>> I disagree technically with Pat below that classes and objects are the *same* thing in f-logic or common-logic, if you intend a class to be a proper set.
> 
> Strictly, a class has a set as its extension.  But Im afraid that technically, a class and an object ARE the same thing in CL (and RDF. I cannot speak for f-logic). That is, each name has a unique, single denotation, which is an individual (logical sense) thing and is also a class and a property, and indeed is also anything else that it might be required to be by its referring name occurring in some syntactic position in the language. This was exactly how CL was designed.

True, but I said something else. Read what I wrote: classes and objects are the same thing BUT (let me be sloppy here - you say it better below) they would not obey a classical set theory in the interpretation - they are sort of disconnected from the real one. If they were, you would have a HOL. I don't want to start a discussion here - and please don't! I JUST want to say that we have here three options wrt a semantics for "confusing" classes and objects: (in an order from the weaker to the stronger) punning (contextual FOL), f-logic (or common logic), high-order (2nd order) logic. Punning - being the weakest - is also the one that gives less interesting inferences.

>> To model exactly this case you need a proper high-order logic
> 
> No, I disagree. You do not need a higher-order logic to model this. There is nothing in the the Tarskian model theory of FO logic that prevents universes of interpretations containing such things as sets, properties or classes. Indeed, many axiomatized set theories are themselves purely first order. The difference between higher-order and first-order logic is, that the HO logics (form 2nd on up, and including the first-order Henkin version) all impose comprehension principles upon the universe. They all require the universe to contain things because it contains other things. Classical HO logic requires it to contain its own power set. Henkin requires it to be closed under lambda-abstraction. And so on. The key thing that makes CL first order is that it imposes no such requirements. It only requires that every name have a denotation. 

True, true, true. But see above. My only point was to emphasise the existence of those three levels.
And that in RDF(S) this difference can not be noticed, and that's why it works elegantly, while in OWL-DL the difference is notable.

cheers
--e.

> 
> To illustrate how this cashes out in practice, consider the following example. From these axioms:
> 
> (P a)
> (Q b)
> 
> does it follow that 
> 
> (exists (p)(and (p a)(p b)))  ?
> 
> In classical HOL - in fact, in 2nd order, even in Henkin logic - it does: the p that makes this be true is 
> 
> (lambda (x)(or (P x)(Q x)))
> 
> In CL it does not, because there is no reason in CL to assume that this property exists. Of course, if you actually define it by writing an axiom:
> 
> (forall (x)(iff (ORPQ x)(or (P x)(Q x)) ))
> 
> and add this to the axiom set, then the conclusion will follow, but now by purely first-order reasoning.
> 
> 
>> , while f-logic or common-logic are a syntactic variant of first-order logic. Nonetheless, I am with Pat when I say that the f-logics semantics is very useful and interesting compromise in the middle.
>> Again, remember that, as also Michael tried to explain with the cases in DBPedia, using punning in OWL-DL leads to a substantial difference in the behaviour wrt the f-logic-like or proper high-order behaviour. 
> 
> The key difference (in fact, the only real difference) is that OWL punning allows identity to be fractured, so that A can be sameAs B viewed as individuals but they be not identical viewed as classes. What this means is that owl:sameAs in OWL 2 is no longer real logical identity: it has been compromised by the punning rules. IMO it would have been better for OWL 2 to have changed the meaning of owl:sameAs so that it retained the strongest possible reading (ie, same individual, same class and same property) and introduced a special weaker identity, perhaps owl:sameIndividual, to be the simple identity in the object universe. With this design, the differences between punning and the RDF/CL semantics are virtually invisible.  Oh well. 
> 
> Pat
> 
>> cheers
>> --e.
>> 
>> On 18 Nov 2010, at 18:25, Pat Hayes wrote:
>> 
>>> 
>>> On Nov 17, 2010, at 4:13 AM, Rinke Hoekstra wrote:
>>> 
>>>> Hi Pavel,
>>>> 
>>>> On 16 nov 2010, at 17:50, Pavel Klinov wrote:
>>>>> As for OWL 2, I do agree with Enrico. Punning is a not quite a logical
>>>>> pattern - it's a meta-modeling feature and has to be used with care.
>>>>> If you pun an object X and a class X they will still be treated as
>>>>> separate entities by a reasoner ("X-as-class" and "X-as-individual" if
>>>>> you will). It can be confusing, for example, one may place a data
>>>>> property assertion on X (as an individual) and then wonder why other
>>>>> instances of X (as a subclass) do not inherit that property.
>>>> 
>>>> This is indeed what happens if you use punning. However, if you interpret it as OWL 2 Full (without punning), the inheritance wouldn't occur either. 
>>>> 
>>>> The fact that some language feature may be confusing is not a very good general argument against using it. 
>>>> 
>>>>> At the
>>>>> same time other tools, like Protege, may give a false impression that
>>>>> "these are really the same thing".
>>>> 
>>>> Hm, but for all practical purposes they *are* the same thing, they are just interpreted differently dependent on context. OWL 2 DL reasoners may separate these contexts for efficiency purposes, but an RDFS/OWL 2 Full reasoner or RDF query engine won't. 
>>>> 
>>>> This is fine if you ask me... I have yet to come across a situation where this potential confusion had any practical consequences. 
>>> 
>>> And in OWL full and RDF and ISO Common Logic, they really ARE the very same thing, with no 'punning' involved. Check out the model theory. Everything in the universe is an individual and a class and a property (and in CL, also a relation and function of every possible arity; and in IKL, which extends CL, also a proposition.) I call this style of model theory 'pollarding': every individual (logical sense) is provided *by the semantics* with enough branches - enough semantic apparatus - to play any logical role that might be required by the syntactic occurrence of its name. It is a view of the universe which says, in effect, I do not know what 'kind' of thing this entity is, so I will presume (as a matter of logic) that it might be any kind, or several kinds, of entity, and be prepared to interpret it thus. It is a kind of rigorous metaphysical agnosticism, and the logic is built on this as a fundamental principle. I feel, in fact, that this is the core of what makes FO logic truly first-order: it is the only logic which makes absolutely no ontological presumptions or constraints on the entities that it talks about. BUt no doubt this is getting to deep for an email discussion :-)
>>> 
>>> Cheers
>>> 
>>> Pat
>>> 
>>>> 
>>>> Cheers,
>>>> 
>>>> Rinke
>>>> 
>>>>> Apologies if I'm mistaken in my understanding of punning.
>>>>> 
>>>>> Cheers,
>>>>> Pavel
>>>>> 
>>>>> On Tue, Nov 16, 2010 at 3:08 PM, Pat Hayes <phayes@ihmc.us> wrote:
>>>>>> 
>>>>>> On Nov 16, 2010, at 4:22 AM, Marco Colombetti wrote:
>>>>>> 
>>>>>>> Aldo is right, punning is allowed in OOWL2, but I wonder whether it should be considered as good practice. In my opinion it conceils certain important modelling choices, and is likely to induce confusion.
>>>>>>> 
>>>>>>> Any strong opinion about this?
>>>>>> 
>>>>>> Yes, one strong opinion: it is VERY good practice. The ISO Common Logic framework goes slightly further, allowing any 'thing' to be treated simultaneously as an individual, a class or a relation ('property') of any number of arguments; and we have found in many applications that the resulting freedom to express ontological decisions independently from the apparent constraints of the logic is more than 'good' : it represents a quantum jump in ontology engineering.
>>>>>> 
>>>>>> The key point is that 'individual' in a metaphysical sense is one notion, whose merits can be debated; but 'individual' in the logical sense is quite another. The latter means simply 'a member of the universe of discourse' or 'within the scope of quantification'. The traditional 'good practices' typically get these two distinct notions confused, and use syntactic constraints arising from the latter to model the former, to the lasting detriment of good ontological engineering.
>>>>>> 
>>>>>> Pat Hayes
>>>>>> 
>>>>>>> 
>>>>>>> Marco
>>>>>>> 
>>>>> --pavel
>>>>> http://www.cs.man.ac.uk/~klinovp
>>>>> 
>>>> 
>>>> 
>>>> ---
>>>> Dr Rinke Hoekstra
>>>> 
>>>> AI Department         |   Leibniz Center for Law    
>>>> Faculty of Sciences   |   Faculty of Law            
>>>> Vrije Universiteit    |   Universiteit van Amsterdam
>>>> De Boelelaan 1081a    |   Kloveniersburgwal 48      
>>>> 1081 HV Amsterdam     |   1012 CX  Amsterdam        
>>>> +31-(0)20-5987752     |   +31-(0)20-5253497         
>>>> hoekstra@few.vu.nl    |   hoekstra@uva.nl           
>>>> 
>>>> Homepage: http://www.few.vu.nl/~hoekstra
>>>> 
>>>> 
>>>> 
>>>> 
>>>> 
>>>> 
>>> 
>>> ------------------------------------------------------------
>>> IHMC                                     (850)434 8903 or (650)494 3973   
>>> 40 South Alcaniz St.           (850)202 4416   office
>>> Pensacola                            (850)202 4440   fax
>>> FL 32502                              (850)291 0667   mobile
>>> phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes
>>> 
>>> 
>>> 
>>> 
>>> 
>>> 
>> 
>> 
>> 
> 
> ------------------------------------------------------------
> IHMC                                     (850)434 8903 or (650)494 3973   
> 40 South Alcaniz St.           (850)202 4416   office
> Pensacola                            (850)202 4440   fax
> FL 32502                              (850)291 0667   mobile
> phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes
> 
> 
> 
> 
> 
>

Received on Thursday, 18 November 2010 23:39:11 UTC