Math Forum Discussions

Graham Cooper

Posts: 4,495
Registered: 5/20/10

Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Posted: Dec 11, 2012 3:49 PM

Plain Text

On Dec 12, 12:24 am, Dan Christensen <Dan_Christen...@sympatico.ca>
wrote:
> 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.

This is the same:

(p-q) ^ (p->not(q))
----------
~p

But it's not "theory wide".

thm(1)
if( 1, 7 )
if( 5 , 10 )
if( 5 , 6 )
if( and(6,7) , not(10) )

5->10 ./
5->not(10)

OK, that could work,
backchain not(10) <- and(6,7) <- and(1,5) <- 5

-----------------------------------------

if(5,6)
if(5,7)
if(6,10)
if(7,not(10))

This requires forward chaning.

OK it does do proof by contradiction, I think TRANSITIVE IF will work,
but it has to backward chain (using MODUS PONENS) at every step.

TRANSITIVE IF
trif( OLD , NEW , l(L) ) :- if( OLD , NEW ).
trif( OLD , NEW , l(L) ) :- if( OLD , MID ) , trif( MID, NEW , L ).

I thought
(p & any_theorems)->q & (p & any_theorems)->~q
----
~p

might be required to catch all contradictions, but no.

Herc