- From: Dan Connolly <connolly@w3.org>
- Date: Thu, 16 Dec 2004 10:08:34 -0600
- To: Sandro Hawke <sandro@w3.org>
- Cc: www-archive@w3.org
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