Comment on log: vocab

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.

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

Received on Wednesday, 14 April 2004 03:14:37 UTC