Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.
|
|
Math Forum
»
Discussions
»
sci.math.*
»
sci.math
Notice: We are no longer accepting new posts, but the forums will continue to be readable.
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
|
 |
|
|
Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Posted:
Dec 11, 2012 3:49 PM
|
|
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
|
|
|
|