From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>

Date: Mon, 20 May 2002 19:17:45 +0200

To: pfps@research.bell-labs.com

Cc: "www-webont-wg" <www-webont-wg@w3.org>

Message-ID: <OF65B39917.7A971E2D-ONC1256BBF.005DE98E@agfa.be>

Date: Mon, 20 May 2002 19:17:45 +0200

To: pfps@research.bell-labs.com

Cc: "www-webont-wg" <www-webont-wg@w3.org>

Message-ID: <OF65B39917.7A971E2D-ONC1256BBF.005DE98E@agfa.be>

> > > a/ ?x a :R -> ?x a [ owl:complementOf ?x ] > > > b/ ?x a [ owl:complementOf ?x ] -> ?x a :R > > > > > > have been derived. > > > > > > Now assume that > > > Ac/ :R a :R > > > (Why? Well because this is how this proof theory makes progress.) > > > > > > Then from modus ponens, a/ and Ac/ > > > Ad/ :R a :R > > > follows. No, it is :R a [ owl:complementOf :R ] that follows per MP :R a :R ?x a :R -> ?x a [ owl:complementOf ?x ] |- :R a [ owl:complementOf :R ] > > > But our theory includes the implication > > > ?x a ?y , ?x a [owl:complementOf :y] -> FALSE > > > so using modus ponens again > > > Ae/ FALSE OK per MP :R a :R :R a [ owl:complementOf :R ] ?x a ?y , ?x a [owl:complementOf :y] -> FALSE |- FALSE > > > Now the proof theory allows the deduction of the opposite of the > > > assumption, so > > > f/ not ( :R a :R ) > > > follows. which is :R a [ owl:complementOf :R ] but you had derived that already assuming :R a :R > > > And so on. > > > > > > Nowhere is there any indication that anything not permitted has happened. > > > > > > So, what is the problem with the above derivation? It seems to be just as > > > VALID or SOUND as any other derivation. > > > > Well, in a sense it seems like you are building > > two mutual dependent proofs, actually more like > > cyclic proof graphs if that term would exist??? > > We are just trying to write a finite proof tree > > for :R a :R (and we can't write down such a fpt) > > > > -- > > Jos > > I don't see any circularity here. Where do you think that the circularity > arises? Yes, assuming :R a :R you can derive per MP :R a [ owl:complementOf :R ] but what you have assumed should become a (finite) branch of the final proof tree. So let's now assume :R a [ owl:complementOf :R ] and then per MP :R a [ owl:complementOf :R ] ?x a [ owl:complementOf ?x ] -> ?x a :R |- :R a :R but what we have assumed should become a (finite) branch of the final proof tree and all we have can be substituted, so :R a :R ?x a :R -> ?x a [ owl:complementOf ?x ] |- :R a [ owl:complementOf :R ] ?x a [ owl:complementOf ?x ] -> ?x a :R |- :R a :R and that is circular. I really wonder if you can write a final proof tree with non-assumed leafs? -- JosReceived on Monday, 20 May 2002 13:18:22 UTC

*
This archive was generated by hypermail 2.4.0
: Friday, 17 January 2020 23:04:30 UTC
*