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