Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.



Re: A formal counterexample of Ax Ey P(x,y) > Ey Ax P(x,y)
Posted:
Dec 9, 2012 12:39 AM


On Dec 8, 6:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote: > On Dec 9, 9:05 am, Dan Christensen <Dan_Christen...@sympatico.ca> > wrote: > > > > > > > > > > > On Dec 8, 1:58 pm, Graham Cooper <grahamcoop...@gmail.com> wrote: > > > > On Dec 8, 6:14 am, Dan Christensen <d...@dcproof.com> wrote: > > > > > Let the domain of quantification be U = {x, y} for distinct x and y. > > > > > Let P be the "is equal to" relation on U. > > > > > Then Ax Ey P(x,y) would be true since x=x and y=y > > > > > And Ey Ax P(x,y) would be false since no element of U would be equal > > > > to every element of U. > > > > > See formal proof (in DC Proof 2.0 format) athttp://dcproof.com/PopSci.htm > > > > This is a classic Skolem Function example. > > > This problem is central to predicate calculus. Like Russell's Paradox, > > it has spurred various "solutions," Skolem functions being one of > > them. My own DC Proof system is another, more natural one (IMHO). > > > Dan > > Download my DC Proof 2.0 software athttp://www.dcproof.com > > a fine grain solution, but I think relational models, set at a time > reasoning, although there is an intuitive understanding step required, > will be more amenable to formal proofs being so much shorter and in > the range of brute force proof search. 65 steps === n^65 is too big > for a computer to ever come across, and that was a simple quantifier > example. >
You have to give a computer the rules. It's a bit much to expect it to justify them. It takes a brain that have been evolving for billions of years to do that.
Dan Download my DC Proof 2.0 software at http://www.dcproof.com



