RE: Datalog With Only Binary Relations Is Too Weak

> > > > > > >     {{: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)

True, but you can do much better than that:
    (A&(A->B)&(B->C))->C
and since, trivially,
     C -> ((A->B)->C)
your conclusion follows.
BTW, it occurs to me that your original tautology
((A->B)&(B->C))->(A->(B->C))
could have beeen written as
((A->B)&(B->C))->(A->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

I wouldnt say 'be-simplified-to/stand-for' here. A->B can't be said 
to 'stand for' B in any reasonable sense, and it would be invalid to 
simplify an implication to its consequent. What would be reasonable 
to say is that B follows from A and (A->B) taken together: that is 
modus ponens, one of the oldest rules in the book. This rule is 
correct because if A is true, and if (A->B) is also true, then B must 
also be true. Contrariwise, if (A->B) is true and B is false, then A 
must be false (modus tollens, the second-oldest rule in the book); 
but either way, you do have to say that the implication is true, 
since if (A->B) is false then A must be true and B must be false. It 
would also be reasonable to say that if (A->B) is true then it can be 
'read' as a licence to infer B from A; but again, only as long as it 
((A->B)) stays true.

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/~phayes

Received on Wednesday, 21 March 2001 13:07:46 UTC