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 10, 2012 11:54 PM


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 ?
M is unbound so it would match to any subset of theorems... should be possible to code in PROLOG.
Herc



