Date: Dec 11, 2012 9:24 AM Author: Dan Christensen Subject: Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y) 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