Dan,

 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...