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

Re: semantics status of RDF(S)

From: <jos.deroo.jd@belgium.agfa.com>
Date: Tue, 10 Apr 2001 00:37:34 +0100
To: phayes@ai.uwf.edu
Cc: www-rdf-logic@w3.org
Message-Id: <OF540EB242.10ADE62A-ON41256A29.008158CD@bayer-ag.com>


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

[how would you call the class of N3 constructs such as at
maybe we should speak about proof-sentences

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

Well it is a resolution algorithm for binary predicates that
takes care of the (ir)reflexive property of the predicates.
A reflexive property is declared (in N3) as
  :p a e:reflexiveProperty.
(otherwise properties are assumed irreflexive and the
extra test for inequality is carried out).
[For an example using a reflexive relation we refer to

> >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'?

Well ok, maybe we should talk about proof-sentence from now on.
I don't see a direct connection with Gentzen sequents (or
natural deduction or Hilbert proof style).
How exactly? As deep as the deduction had to go, what else?

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

Yes, but I have trouble with meta-things.
It is just simply asking to proof the proof-as-a-propositional-sentence
against the same set as axioms used for the original lemma (or question).

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

but we want to check a proof-as-a-propositional-sentence with
another proof-sentence checker

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

Is that also true for second/higher order logic?

Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Monday, 9 April 2001 18:37:48 UTC

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