```Date: Dec 10, 2012 11:54 PM
Author: Graham Cooper
Subject: Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)

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 counter-example 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 counter-example destroys claims of correct> derivation by virtue of the soundness theorem for> the deductive calculus of first-order logic.OK, going off on a tangent here, what is the domain of this inferenceformula?~p->f & ~p->~f----------------pf,~f |- WFrom a contradiction anything follows, but treats ~p~p -> fin the LHS as an *ASSUMPTION*.===========================I'm trying to get it work similarly to MODUS PONENSl & l->r--------r===========================Here is the problem:Although:~p->f & ~p->~f----------------pit would be a FLUKE to directly match any implied formula f.===========================would(m&~p)->f & (m&~p)->~f----------------pprove p for ALL-CASES  IFF  a contradiction arrives from ~p ?M is unbound so it would match to any subset of theorems... should bepossible to code in PROLOG.Herc
```