In case Axiom Schemas are making you uncomfortable --- they were included merely as a convenience. They are not part of LBase, they are a facility for easily creating Lbase axioms.

As for the issue of sentential variables vs non-sentential variables, that is easy to define ... we could say that we only allow axiom schemas to be instantiated with substitutions of schema variables with one of the constant symbols.

As for the axiom

(forall (?x ?y) (rdf:type(?x, ?y) <=> ?y(?x)))

I am going to let Pat defend that one ... It turns out that in the current model theory for RDF, Class membership is modelled as a unary relation. This axiom is to make the Lbase axiomatization symmetric with the rdf mt.

As for not using the rule of the excluded middle, etc. --- This is a much bigger issue than axiomatic approaches vs model theoretic approaches. The current model theories, from webont & rdf, do assume the law of the excluded middle. If we leave that out, we will be quite far outside the scope of classical logics. I have no idea where to even begin broaching such questions in the W3C process.

guha

Dan Connolly wrote:

On Wed, 2002-06-12 at 16:01, R.V.Guha wrote: [...]I would like to get a wider sample, especially from the folks building stuff (like Libby, Connolly, ...).I prefer an axiomatic approach inasmuch as it allows me to use the machine to check my work etc. I'm stil mulling over details of this approach; in particular, stuff like "Axiom schemes do not take the language beyond first-order, since all the instances are first-order sentences and the language is compact, so if any Lbase sentence follows from (the infinite set of instances of) an axiom scheme, then it must in fact be entailed by some finite set of instances of that scheme. " -- http://tap.stanford.edu/SemanticWebSemantics.html give me pause, as does: "Since relations are first-class entities in Lbase, we can express this relationship with an axiom: (forall (?x ?y) (rdf:type(?x, ?y) <=> ?y(?x))) " -- http://www.coginst.uwf.edu/%7Ephayes/RDF%28S%29_based_on_Lbase.html I agree with Graham that... "- in the description of axiom schemata, it is not clear how one is expected to distinguish "schematic variables" from non-substitutable values." I'm quite happy with the "menzel indrection trick" in the present model theory. I'm still noodling on the corresponding bits of the Lbase stuff. Another technical reservation I have is committing to classical negation. Based on discussion with TimBL and study of systems like Isabelle, I don't think the law of the excluded middle is a good thing to commit to for the semantic web. http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ I have to admit that I can't think of a way to make these issues show up in RDF 1.0 nor RDFS. But the premise of this approach is that the same base logic works for higher layers too. Maybe I'll noodle on some test cases that involve webont-ish vocabulary... oops; stuff exploding around here; gotta go...