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 ]
Dan Christensen

Posts: 2,866
Registered: 7/9/08
Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Posted: Dec 11, 2012 9:24 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Dec 10, 11:54 pm, Graham Cooper <grahamcoop...@gmail.com> 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 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 ?
>


I'm not sure what you are trying to do, but, for proof by
contradiction in propositional logic, I use the rule:

p |- (q & ~q)
---------------
~p <--- Conclusion statement

where p is a Premise and ~p is the Conclusion.

It gets a little more complicated if free variables were introduced in
p. Then...

p |- (q & ~q)
--------------
~E x1,... xn p <--- Conclusion statement

where the xi are the free variables introduced in p. (Not sure if I am
using the notation here correctly. I just program it!) In general, no
new free variables that were introduced in p or subsequently (by E
Spec) will appear in the conclusion. This saves all kinds of
headaches!

For direct proof:

p |- q
--------------
A x1,... xn [p -> E y1,... yn q] <--- Conclusion statement

where the xi are the free variables introduced in p, and the yi are
the free variables subsequently introduced by Existential
Specification that remain in q. This is the only way to do a Universal
Generalization in DC Proof. In DC Proof, new free variables can only
be introduced by a Premise or E Spec Rules -- NOT by Universal
Specification. It's just FOL with some "guidelines" (restrictions)
built in to make it easier to do mathematical proofs (like structured
programming introduced in the 1970's).

Dan
Download my DC Proof 2.0 software at http://www.dcproof.com



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.