- From: <jos.deroo.jd@belgium.agfa.com>
- Date: Tue, 20 Mar 2001 22:42:18 +0100
- To: phayes@ai.uwf.edu
- Cc: www-rdf-logic@w3.org
> > > > > > {{:gregorian :grandparent :bret} log:implies
> > > > > > {{:gregorian :skolemfun :bret} :parent :bret}} log:implies
> > > > > > {{:gregorian :skolemfun :bret} a :isLoved}.
> > > > >
> >.....
> > > The above appears to have the overall structure
> > > (A implies B) implies C
> > > which is rather unlikely, if 'log:implies' means logical implication,
> > > because that is equivalent to the conjunction
> > > (A or C) and (B implies C)
> >
> >Of course, how could I be so stupid ...
> >If we assume following axioms
> > A->B i.e. A log:implies B.
> > B->C
> >then the proof of C should look like
> > A->(B->C)
> >and not like I've done so far!
> >Only then we have the tautology
> > ((A->B)&(B->C))->(A->(B->C))
> >isn't it?
>
> Yes, that follows, but kind of trivially, since if (B->C) then
> (A->(B->C)) no matter whether A is true or false. And the reverse:
> *** ((A->B)&(B->C)) <- (A->(B->C))
> is not valid.
> I think the equivalence you want might be this:
> ((A&B)->C) <-> (A->(B->C))
> which is both valid and nontrivial (?)
OK
(stupid | not-stupid) ->
(A&(A->B)&(B->C))->((A->B)->C)
also (if we don't have qualified variables)
A is true by fact
A->B can be-simplified-to/stand-for B which is also true
B->C can be-simplified-to/stand-for C which is also true
--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Tuesday, 20 March 2001 16:42:44 UTC