Re: semantics status of RDF(S)

[...]

> >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
  http://www.agfa.com/w3c/euler/authen.proof.n3
  http://www.agfa.com/w3c/euler/bless.proof.n3
  http://www.agfa.com/w3c/euler/define.proof.n3
  http://www.agfa.com/w3c/euler/extra.proof.n3
  http://www.agfa.com/w3c/euler/gedcom-proof.n3
  http://www.agfa.com/w3c/euler/graph.proof.n3
  http://www.agfa.com/w3c/euler/lists.proof.n3
  http://www.agfa.com/w3c/euler/russell.proof.n3
]
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
  http://www.agfa.com/w3c/euler/graph.axiom.n3
  http://www.agfa.com/w3c/euler/graph.lemma.n3
  http://www.agfa.com/w3c/euler/graph.proof.n3
  http://www.agfa.com/w3c/euler/graph.check.n3
]

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