From: pat hayes <phayes@ai.uwf.edu>

Date: Mon, 9 Apr 2001 12:01:37 -0500

Message-Id: <v04210107b6f798e826c4@[130.107.66.237]>

To: jos.deroo.jd@belgium.agfa.com

Cc: www-rdf-logic@w3.org

Date: Mon, 9 Apr 2001 12:01:37 -0500

Message-Id: <v04210107b6f798e826c4@[130.107.66.237]>

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 >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/~phayesReceived 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
*