Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.


Math Forum
»
Discussions
»
sci.math.*
»
sci.math
Notice: We are no longer accepting new posts, but the forums will continue to be readable.
Topic:
A formal counterexample of Ax Ey P(x,y) > Ey Ax P(x,y)
Replies:
5
Last Post:
Dec 11, 2012 3:49 PM




Re: A formal counterexample of Ax Ey P(x,y) > Ey Ax P(x,y)
Posted:
Dec 11, 2012 3:49 PM


On Dec 12, 12:24 am, Dan Christensen <Dan_Christen...@sympatico.ca> wrote: > On Dec 10, 11:54 pm, Graham Cooper <grahamcoop...@gmail.com> wrote: > > > > > > > > > > > On Dec 10, 2:31 pm, fom <fomJ...@nyms.net> wrote: > > > > On 12/8/2012 11:13 PM, Dan Christensen wrote: > > > > > On Dec 8, 7:05 pm, fom <fomJ...@nyms.net> wrote: > > > >> On 12/8/2012 4:58 PM, Dan Christensen wrote: > > > > <snip> > > > > > I am proving that Ey Ax P(x,y) does not follow from Ax Ey P(x,y). > > > >  AxAyAz((x=y /\ y=z) > x=z) > > >  AxAy(x=y > y=x) > > >  (d=c) > > >  AxEy(x=y) > EyAx(x=y) > > >  AxEy(x=y) > > >  Ey(p=y) > > >  p=c > > >  EyAx(x=y) > > >  Ax(x=d) > > >  p=d > > >  Ay(p=y > y=p) > > >  p=d > d=p > > >  d=p > > >  AyAz((d=y /\ y=z) > d=z) > > >  Az((d=p /\ p=c) > d=c) > > >  (d=p /\ p=c) > d=c > > >  d=p /\ p=c > > >  d=c > > >  d=c /\ (d=c) > > > > That is what the proof of your revised statement > > > looks like. And, contrary to your fast and impatient > > > response, it requires a formal assumption of > > > distinctness as George brought to your attention > > > elsewhere. > > > > Your model is a counterexample to any purported > > > proof of the original statement. With a model you > > > are proving that EyAx(x=y) is not a logical consequence > > > of AxEy(x=y). Logical consequence is a semantic > > > notion. A counterexample destroys claims of correct > > > derivation by virtue of the soundness theorem for > > > the deductive calculus of firstorder logic. > > > OK, going off on a tangent here, what is the domain of this inference > > formula? > > > ~p>f & ~p>~f > >  > > p > > > f,~f  W > > > From a contradiction anything follows, but treats ~p > > > ~p > f > > > in the LHS as an *ASSUMPTION*. > > > =========================== > > > I'm trying to get it work similarly to MODUS PONENS > > > l & l>r > >  > > r > > > =========================== > > > Here is the problem: > > > Although: > > > ~p>f & ~p>~f > >  > > p > > > it would be a FLUKE to directly match any implied formula f. > > > =========================== > > > would > > > (m&~p)>f & (m&~p)>~f > >  > > p > > > prove p for ALLCASES IFF a contradiction arrives from ~p ? > > I'm not sure what you are trying to do, but, for proof by > contradiction in propositional logic, I use the rule: > > p  (q & ~q) >  > ~p < Conclusion statement > > where p is a Premise and ~p is the Conclusion.
This is the same:
(pq) ^ (p>not(q))  ~p
But it's not "theory wide".
thm(1) if( 1, 7 ) if( 5 , 10 ) if( 5 , 6 ) if( and(6,7) , not(10) )
5>10 ./ 5>not(10)
OK, that could work, backchain not(10) < and(6,7) < and(1,5) < 5

if(5,6) if(5,7) if(6,10) if(7,not(10))
This requires forward chaning.
OK it does do proof by contradiction, I think TRANSITIVE IF will work, but it has to backward chain (using MODUS PONENS) at every step.
TRANSITIVE IF trif( OLD , NEW , l(L) ) : if( OLD , NEW ). trif( OLD , NEW , l(L) ) : if( OLD , MID ) , trif( MID, NEW , L ).
I thought (p & any_theorems)>q & (p & any_theorems)>~q  ~p
might be required to catch all contradictions, but no.
Herc



