- From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>
- Date: Mon, 20 May 2002 16:24:02 +0200
- To: pfps@research.bell-labs.com
- Cc: "www-webont-wg" <www-webont-wg@w3.org>
> I'm still trying to understand this table. I'll add in some extra > information to see if I can clarify it. > > Premise -> Conc. > * a a->b b Deducing b from a and a->b > * using modus ponens > ---------------------------------------------------- > (1) False True False VALID UNSOUND > (2) False True True VALID UNSOUND > (3) True False False INVALID UNSOUND > (4) True True True VALID SOUND Right > > and having that > > :R a [ owl:complementOf :R ] > > is the same proposition as > > not(:R a :R) > > we have the case > > not(p) -> p > > so only (2) or (3) are to be considered > > but both are UNSOUND > > So what is the situation with respect to these formulae. Well, there needs > to be a development of the theory, but let's assume that this has been > done. > > So let's take as given that > > 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 [ owl:complementOf :R ] > follows. > > But our theory includes the implication > ?x a ?y , ?x a [owl:complementOf :y] -> FALSE > so using modus ponens again > Ae/ FALSE > > Now the proof theory allows the deduction of the opposite of the > assumption, so > f/ not ( :R a :R ) > > follows. > > 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
Received on Monday, 20 May 2002 10:25:10 UTC