Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
|
|
Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Posted:
Dec 10, 2012 11:54 PM
|
|
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
|
|
|
|
