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.independent

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 ]
fom

Posts: 1,969
Registered: 12/4/12
Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Posted: Dec 11, 2012 12:44 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On 12/10/2012 10:54 PM, Graham Cooper 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
>


oddly enough, this is presupposition

-p entails the interpretation of f as a proposition



~p->f & ~p->~f
-True(f)
-False(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.