```Date: Dec 13, 2012 3:44 AM
Author: Graham Cooper
Subject: Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)

On Dec 13, 1:41 pm, Dan Christensen <Dan_Christen...@sympatico.ca>wrote:> On Dec 12, 6:54 pm, Jan Burse <janbu...@fastmail.fm> wrote:> > Here is an example where the above method gives a false> > positive:>> > Your system should be able to prove:>> >     ~p & (~p -> p) -> ~p>> Easy.>>         1       ~P & [~P => P]>                 Premise>>         2       ~P>                 Split, 1>> 3       ~P & [~P => P] => ~P>         Conclusion, 1>> > But we do not have:>> >     ~p & (~p -> p) |/- p>> > In fact by modus ponens it is easy to see that p> > derives from ~p & (~p -> p).>> Also easy.>>         1       ~P & [~P => P]>                 Premise>>         2       ~P>                 Split, 1>>         3       ~P => P>                 Split, 1>>         4       P>                 Detach, 3, 2>> 5       ~P & [~P => P] => P>         Conclusion, 1>> Sorry, I don't see your point, Jan. 3       ~P & [~P => P] => ~P 5       ~P & [~P => P] => PThis would definitely qualify for G.I.G.O. though!So is a MODEL FINDER required to detect this contradiction?I would have thought a MP style contradiction rule would work..~p->f & ~p->~f----------------pI think I can get this running in the same Theorem Prover programusing a transitive -> rule.1st I want to test out AXIOM BASED Modus Ponens with TransitiveImplication.BACKWARD CHAINED - FORWARD BRANCHING MPt(NEW,l(L)) :- trif(AXIOM,NEW,L), t(AXIOM,1).TRANSITIVE IFtrif( OLD , NEW , l(L) ) :- if( OLD , NEW ).trif( OLD , NEW , l(L) ) :- if( OLD , MID ) , trif( MID, NEW , L ).***********STANDARD MPt(NEW,l(L)) :- if(OLD,NEW) , t(OLD,L).branches lower and lower eventually reaching an axiom.Herc
```