Re: Comment on log: vocab

On Wed, 2004-04-14 at 02:12, Jeremy Carroll wrote:
> Hi Tim, Dan,
> 
> apologies for rather formal tone here, I think it may be clearer than an 
> informal tone. This is essentially a bug report with suggested fix. 
> I suspect it is of wider interest, hence the www-rdf-logic CC.

Makes sense to me, but I can't speak for TimBL with confidence here.
I hope he'll respond in due course.

> This is a comment on:
> 
> http://www.w3.org/2000/10/swap/log
> 
> Summary:
> 
> If this vocab is understood as logical rather than proof theoretic then it is 
> inconsistent. Suggest changing rdfs:comments to prioritise proof theoretic 
> reading.
> 
> A few sample suggested changes:
> 
> OLD
> log:Truth a rdfs:Class;
>     rdfs:comment """Something which is true: belive it as you would belive 
> this.
> 	       Understood natively by cwm in that it will execute rules in a formula
>          declared a Truth within a formula it is already taking rules 
> from.""".
> 
> NEW
> log:Truth a rdfs:Class;
>     rdfs:comment """Something which is provable or axiomatically true: 
>                         believe it as you would believe this.
> 	       Understood natively by cwm in that it will execute rules in a formula
>          declared a Truth within a formula it is already taking rules 
> from.""".
> 
> 
> OLD:
> 
> log:implies a rdf:Property;
>     rdfs:comment """Logical implication.
> This is the relation between the antecedent (subject) and
> conclusion (object) of a rule.
> For every subsitution of variable names for symbols or literals
> which maps the antecedent to a fromula which knowledge base
> log:includes, the same substitution is applied to the
> conclusion to generate the result.
> 
> Used by cwm as the basic hook for adding inference to RDF.
> See the manual to define what the knowledge base is and
> where the results go. See also log:conclusion.""";
> 
> NEW
> 
> 
> log:implies a rdf:Property;
>     rdfs:comment """The provability relationship.
> This is the relation between the antecedent (subject) and
> conclusion (object) of a rule.
> For every subsitution of variable names for symbols or literals
> which maps the antecedent to a fromula which knowledge base
> log:includes, the same substitution is applied to the
> conclusion to generate the result.
> 
> Used by cwm as the basic hook for adding inference to RDF.
> See the manual to define what the knowledge base is and
> where the results go. See also log:conclusion.""";
> 
> 
> ============
> 
> Rationale. It is possible to use rdfs:comment to introduce a contradiction 
> when the comment is understood as constraining the class or property (as is 
> the intent). e.g.
> 
> eg:Russell a rdfs:Class;
>   rdfs:comment """The class of all classes that do not have themselves as a 
> type. i.e. ?x a eg:Russell if and only if not ?x a ?x""" .
> 
> This appears to be just normal RDF (no N3 extensions), but is seriously 
> flawed. There are no interpretations for which the comment, understood in 
> English, describes the class eg:Russell.
> 
> Similarly the current description of log:implies as "Logical implication" is 
> flawed since there are no interpretations that make it true as shown by the 
> liar paradox that I posted earlier:
> http://lists.w3.org/Archives/Public/www-rdf-logic/2003Nov/0040
> 
> @prefix log: <http://www.w3.org/2000/10/swap/log#> .
> @prefix owl: <http://www.w3.org/2002/07/owl#> .
> { 
>   <http://example.org/liar> 
>        log:implies { 
>     <http://example.org/noone> a owl:Nothing .
>   } . 
> } owl:sameAs <http://example.org/liar> .
> <http://example.org/liar> a log:Truth .
> 
> See also Pat's posting on the rules list:
> http://lists.w3.org/Archives/Public/www-rdf-rules/2002Dec/0003
> 
> A better fix would be to whole-heartedly embrace proof theoretic and define 
> these terms using an abstract proof theory rather than a concrete proof 
> machine (CWM). i.e. I see text like:
> """Used by cwm as the basic hook for adding inference to RDF.
> See the manual to define what the knowledge base is and
> where the results go. See also log:conclusion."""
> as essentially OK, and a good foundation on which to build a more abstract 
> definition of a proof theoretic nature: log:implies is essentially practical 
> not logical.
> 
> Jeremy
> 
> 
> 
-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
see you at the WWW2004 in NY 17-22 May?

Received on Thursday, 15 April 2004 12:59:34 UTC