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