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


fom
Posts:
1,968
Registered:
12/4/12


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


On 12/10/2012 10:54 PM, Graham Cooper 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 >
oddly enough, this is presupposition
p entails the interpretation of f as a proposition
~p>f & ~p>~f True(f) False(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 >



