Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math

Topic: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Replies: 5   Last Post: Dec 11, 2012 3:49 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Graham Cooper

Posts: 4,348
Registered: 5/20/10
Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Posted: Dec 10, 2012 11:54 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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



Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.