Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
fom
Posts:
1,037
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
|
|
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
>
|
|
|
|
