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



Re: A formal counterexample of Ax Ey P(x,y) > Ey Ax P(x,y)
Posted:
Dec 11, 2012 9:24 AM


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.
It gets a little more complicated if free variables were introduced in p. Then...
p  (q & ~q)  ~E x1,... xn p < Conclusion statement
where the xi are the free variables introduced in p. (Not sure if I am using the notation here correctly. I just program it!) In general, no new free variables that were introduced in p or subsequently (by E Spec) will appear in the conclusion. This saves all kinds of headaches!
For direct proof:
p  q  A x1,... xn [p > E y1,... yn q] < Conclusion statement
where the xi are the free variables introduced in p, and the yi are the free variables subsequently introduced by Existential Specification that remain in q. This is the only way to do a Universal Generalization in DC Proof. In DC Proof, new free variables can only be introduced by a Premise or E Spec Rules  NOT by Universal Specification. It's just FOL with some "guidelines" (restrictions) built in to make it easier to do mathematical proofs (like structured programming introduced in the 1970's).
Dan Download my DC Proof 2.0 software at http://www.dcproof.com



