- From: pat hayes <phayes@ai.uwf.edu>
- Date: Mon, 16 Apr 2001 11:14:18 -0500
- To: Graham Klyne <GK@ninebynine.org>
- Cc: www-rdf-logic@w3.org
>Pat, > >Thanks for your comments. At this point, I wish to stand back a >little and, rather than defend my suggested "stack", to focus on the >issues I was hoping to draw out... > >... I think I'm getting an inkling of the added dimension of >"semantics". It appears I might have been confusing semantics with >structure (a rather elementary error, it now seems). > > >Let's see if I'm getting even remotely close here: the "lower" >layers of the structure I mentioned previously are almost entirely >concerned with structure. Referring to the Formal Systems >Definitions page that Dan C cited a while ago >(http://www-rci.rutgers.edu/~cfs/305_html/Deduction/FormalSystemDefs.h >tml), I tried to fit the rather trivial case of bits and octets into >this framework and what I noticed was that there was no distinction >among those things that constitute a well formed formula (i.e. for >octets, a wff is a sequence of 8 bits): there is no further notion >of axioms or inference: the closest I could get was to say that >*all* wffs were also axioms, which leaves nothing to infer. > >So, if I'm on the right track, semantics only come into play when one: >- can reasonably/justifiably designate some subset of wffs as axiomatic >- introduces rules of inference that relate consequent wffs to some >antecedent wffs. Well, not quite. Logical semantics (model theory) applies as soon as one has a notion of wff. Often the most useful way to define a language is to first define its grammar (wffs) then define its model theory, and only then think about rules of inference, axioms, etc. (what logicians call proof theory). (That is how KIF is being defined, for example.) The reason being that there are usually many, many alternative proof theories (different formal systems) for the same language, and the choice between them is best made on all kinds of pragmatic or computational or even aesthetic grounds; but the syntax and the model theory are what determine the essential logical properties of the language. That is what makes it first-order or higher-order, what makes it computable or decideable or whatever. The particular axioms and rules can differ from one site to another, but as long as they are all compatible with the model theory (all axioms valid, all rules correct), it wouldn't matter a damn that they were using different axioms or notions of proof. >Then there is the assignment of concepts to symbols so that there is >some kind of correspondence between the theory and some states of >affairs - the "model theory"? Yes, exactly. But that can be done independently of the axioms and rules of inference. > >[[[ >QUESTION: how are the axioms and rules of inference different from >the symbols and rules of construction for wffs? > symbols + syntax rules -> wffs > axioms + inference rules -> theorems >]]] The wffs are defined by the grammar of the language. Parsers detect wellformedness. Being wellformed says nothing about the truthvalue, however. "(P and (not P))" is wellformed but contradictory. Axioms are wffs that are asserted, or assumed, to be true. Rules of inference allow something to infer theorems from other theorems (this terminology seems a bit antiquated to me, by the way). An axiom is valid if it is always true (ie true in every possible interperetation.) A rule is correct if its conclusions are true whenever the assumptions are. >Working up the "stack" the first hint of WFFs being not all equally >valid seems to come with XML, which has "validity constraints" as >well as "well formedness constraints" -- does this admit the idea of >valid XML documents as the axioms of a formalism based on XML? I >think not: I think the validity constraints are more reasonably >viewed as additional structural requirements that cannot be >expressed by a context-free grammar. Yes, I agree. I think that is a pun on 'valid'. XML isn't using the terminology of logic. > >[[[BTW, I view the suggested layering to be, at best, a "projection" >of one view of some components that may be combined to achieve the >kind of target function (I think) we're after. Others will almost >certainly have different views. As a system architect, I find it >very useful to try and tease apart components of a complex system >that can be designed in (relative) isolation. Whether that results >in a stack, or tree, or something else is not of primary import >here.]]] > >Somewhere in the RDF(S) components it seems to be reasonable to >start distinguishing between RDF graphs that are "believed true", >and those which aren't, and looking for some rules of deduction. >This does appear to be a very different kind of idea to the purely >structural relationships of the underlying layers (though I'm still >gnawing at the question above). What makes the crucial difference is that the well-formedness constraint can be computed by looking at the expression in isolation, whereas being a theorem cannot be checked by a local computation, but requires a search through a potentially infinite space of possible derivations (ie proofs). >... > >>That is exactly what the description-logic community have been >>studying in depth for the last decade. There are some results, some >>usable systems have been designed and implemented, and a lot of >>tough theoretical problems remain. Maybe y'all should do some >>reading; it will save a lot of time in the long run. > >I'm sure you're right... can you recommend anything in particular? >(Preferably accessible -- not assuming too much background, and >relevant to the current topic.) My searches on Amazon/Google have >failed to turn up anything that looks obviously promising as >introductory material. Check out the CLASSIC web page at Lucent for useful readings and pointers to other, related, projects. (I am off-web right now so can't give you the URL, but I used Google to find it. Also you can toss 'description logic' at Google and find some useful sites full of readings, pointers etc.) If anyone else can suggest some good intro reading on description logics for logical beginners, by the way, please speak up. Deborah, Peter, Ian? >I just dug out your papers "In defense of logic" and "The second >naive physics manifesto" (I happen to have copies to hand) and these >have helped me understand something of the significance of >interpretation as part of semantics; viewpoints from other >commentators, and a concise introduction to the logic formalisms >involved (especially covering the model theory for FOL) might be >helpful. I will try to find (or write) something. >And also, a working definition of "semantics" might help. It is a dangerous word, to be sure. I am using it in the sense it is used in formal logic, ie to refer to model theory. (It is used in a rather wider sense by philosophers of language, semioticians, and others.) Pat Hayes --------------------------------------------------------------------- IHMC (850)434 8903 home 40 South Alcaniz St. (850)202 4416 office Pensacola, FL 32501 (850)202 4440 fax phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes
Received on Monday, 16 April 2001 14:19:16 UTC