Re: semantics status of RDF(S)

> > >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
>http://www.w3.org/2001/Talks/0228-tbl/slide5-0.html

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

Indeed.

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

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 
proof-metalanguage?)

>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
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Monday, 9 April 2001 14:59:30 UTC