W3C home > Mailing lists > Public > www-rdf-logic@w3.org > April 2001

Re: semantics status of RDF(S)

From: pat hayes <phayes@ai.uwf.edu>
Date: Mon, 9 Apr 2001 12:01:37 -0500
Message-Id: <v04210107b6f798e826c4@[]>
To: jos.deroo.jd@belgium.agfa.com
Cc: www-rdf-logic@w3.org
> > >There is however an easier problem (maybe).
> > >On the proof level (where proof expressions live)
> > >we can discover that p has a no-proof-found value.
> > >Of course that is not the denial of p but that
> > >is not a problem for a proof expressions's life!
> > >All it has to express is evidence that can be
> > >syntactically checked to give semantic validity
> > >(and such expressions can contain p->false
> > >parts coming from negated premisses).
> >
> > I have no idea what you are talking about in the above paragraph. Can
> > you rephrase it? In particular, what is the 'proof level' ?
>I see that our phrasing is indeed ussuming a lot of
>implicit things ...
>The proof level is what TimBL has drawn so nicely in

As I said, that is simply a picture. It has no precise meaning that I 
can determine.

>We also assume a proof expression to be a propositional
>logic formula.

Wait a minute. A *proof* is a *formula*? That sounds like a category 
mistake. Eg resolution proofs are trees, not formulae. (Maybe you 
could give an example to show what you are talking about?)

>Of course this is not yet a proof language!
>Such a proof can be the result of e.g. predicate logic
>inferences (using e.g. binary predicate reflexive resolution,

"reflexive" resolution? What is that?

>but of course there are many, many proof engine technologies).


>I want to refer here to the stuff that we have exemplified
>at http://www.agfa.com/w3c/euler/ (just to fix the idea).
>In there the so called proofs are nested material

A material implication is a sentence, not a proof. (Do you mean 
something like a Gentzen sequent?). Also, how exactly are the 
material implications 'nested'?

>If those proofs are posed as a new lemma

What does it mean to pose a proof as a lemma? A proof doesnt assert 
anything, so it can't be proved. (Do you mean that the 
well-formedness of the proof is proved in some kind of 

>one obtains a so called checked proof (which is actually
>a fixpoint when also posed as a lemma).
>A checked proof is somehow giving the syntactic validity
>  axioms |- lemma

That is what a proof does already, so where does the "checked" come in?

>and as we know from symbolic logic
>  syntactic validity |- implies semantic validity |=

That is a definition of correctness, yes.

>  (but not necessarily the other way around according to
>  an interpretation of Goedel's incompleteness theorem).

No. First, the other way round IS satisfied by a complete inference 
system (eg resolution, suitably understood). Second, this has nothing 
whatever to do with Goedel's incompleteness theorem (which was 
concerned with the incomplteness of arithmetic, not logic).

Pat Hayes

IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
Received on Monday, 9 April 2001 14:59:30 UTC

This archive was generated by hypermail 2.3.1 : Wednesday, 2 March 2016 11:10:34 UTC