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.
It gets a little more complicated if free variables were introduced in p. Then...
p |- (q & ~q) -------------- ~E x1,... xn p <--- Conclusion statement
where the xi are the free variables introduced in p. (Not sure if I am using the notation here correctly. I just program it!) In general, no new free variables that were introduced in p or subsequently (by E Spec) will appear in the conclusion. This saves all kinds of headaches!
For direct proof:
p |- q -------------- A x1,... xn [p -> E y1,... yn q] <--- Conclusion statement
where the xi are the free variables introduced in p, and the yi are the free variables subsequently introduced by Existential Specification that remain in q. This is the only way to do a Universal Generalization in DC Proof. In DC Proof, new free variables can only be introduced by a Premise or E Spec Rules -- NOT by Universal Specification. It's just FOL with some "guidelines" (restrictions) built in to make it easier to do mathematical proofs (like structured programming introduced in the 1970's).