Re: same-syntax extensions to RDF

On Thu, 2004-12-16 at 10:47 -0500, Sandro Hawke wrote:
> > On Thu, 2004-12-16 at 00:11 -0500, Sandro Hawke wrote:
> > [...]
> > > So most of the LX ontology is just a straightforward transcription of
> > > a textbook description of FOL syntax into the slightly odd world of
> > > RDF triples, where rather than the BNF
> > > 
> > >     <conjunction> ::= <formula> '&' <formula>
> > > 
> > > we have Conjunction as a class, and two properties conjLeft and
> > > conjRight with domain Formula and range Conjunction.
> > 
> > But you also mean to say that "any fin[it]e number of applications
> > of these rules yeilds an element of the class Formula" and such,
> > right? That's a case of "generalization to infinitely many cases".
> >  http://www.w3.org/DesignIssues/Logic#L736
> 
> Isn't that roughly:
> 
>    all Conj (
>       rdf(Conj, rdf_type, lx_Conjunction)
>       <->
>       (  exists Left Right (
>             rdf(Conj, lx_conjLeft, Left),
>             rdf(Conj, lx_conjRight, Right),
> 	    rdf(Left, rdf_type, lx_Formula),
> 	    rdf(Right, rdf_type, lx_Formula)
>          )
>       )
>    ).
> 
> ?   The "any number of applications" notion gets expressed via forall.

Roughly, maybe, but formal systems are all about precision.
Nothing in a "forall" says that every formula is the result
of *finitely many* applications of that axiom.

That axiom is consistent with infinitely large formulas.

There's nothing wrong with that in and of itself, but you
seem to want your intuitions about grammars to carry over;
i.e. that you can prove something about all strings
in the language just by thinking about each production
in the grammar.

I haven't finished learning what "first order" really means...
I understand there's a collection of equivalent results
including the "compactness theorem", much like the equivalent
results about regular expressions and regular grammars.

But I learned the hard way not to treat issues of finiteness
and FOL lightly... by displaying my
ignorance at an OWL ftf meeting where Peter, Ian, Pat,
and company took me to task. Let's see if I can find
minutes...

Ah yes, it was the Standford meeting
http://www.w3.org/2001/sw/WebOnt/ftf3.html

where I presented:

Re: layering (5.3,5.10): a first-order same-syntax model theory Dan
Connolly (Fri, Jun 28 2002)
http://lists.w3.org/Archives/Public/www-webont-wg/2002Jun/0209.html17:04:12

hmm... the hypertest structure of those minutes isn't great,
but see especially the "Model theory break-out" section.



> > i.e. it's not a first-order system.
> 
> I'm not sure the clearest way to talk about the levels, or what
> constitutes "the system".
> 
> My application scenario is that someone wants to transmit FOL
> assertions through an RDF channel.  The RDF channel is subject to the
> usual merging, erasure, open-world, etc, issues.  The end queries will
> be about the presense (entailment) of RDF triples.   
> 
>     Alice wants to say "All greek:man are greek:mortal".
> 
>     She writes that down in FOL, she describes and asserts that FOL
>     in RDF using LX.
> 
>     She sends the RDF triples to Bob.
> 
>     Bob stuffs them into his triples store that implements LX
>     inference.  He also adds "Socrates rdf:type greek:man".  Now he
>     queries whether "Socrates rdf:type greek:mortal" and is told Yes
>     (with provenance pointing to his addition about Socrates and the
>     triples from Alice, and maybe the LX inference machinery).
> 
> Or something like that.  Lots of variations.   
> 
>      -- sandro
> 
>    
-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E

Received on Thursday, 16 December 2004 16:08:19 UTC