Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Replies: 4   Last Post: Dec 9, 2012 12:39 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Dan Christensen

Posts: 2,483
Registered: 7/9/08
Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
Posted: Dec 9, 2012 12:39 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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








Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.