Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Replies: 3   Last Post: Dec 13, 2012 10:02 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Graham Cooper

Posts: 4,227
Registered: 5/20/10
Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Posted: Dec 13, 2012 3:44 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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] => P

This 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
----------------
p


I think I can get this running in the same Theorem Prover program
using a transitive -> rule.

1st I want to test out AXIOM BASED Modus Ponens with Transitive
Implication.

BACKWARD CHAINED - FORWARD BRANCHING MP

t(NEW,l(L)) :- trif(AXIOM,NEW,L), t(AXIOM,1).

TRANSITIVE IF
trif( OLD , NEW , l(L) ) :- if( OLD , NEW ).
trif( OLD , NEW , l(L) ) :- if( OLD , MID ) , trif( MID, NEW , L ).

***********

STANDARD MP
t(NEW,l(L)) :- if(OLD,NEW) , t(OLD,L).

branches lower and lower eventually reaching an axiom.


Herc



Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.