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 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 ALL-CASES 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