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>

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

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:52:38 GMT
*