Date: Dec 8, 2012 1:58 PM
Author: Graham Cooper
Subject: Re: A formal counter-example of Ax Ey P(x,y) -> Ey Ax P(x,y)
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.

A(x) E(y) y>x

replace y with a bigger than function

bigger(x) > x

Rather than a VALUE Y exists,

a SOLUTION EXISTS -> an ALGORITHM BIGGER() EXISTS

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

bigger function as a relation

A(Y):{Y | bigger(Y,X)} Y>X

ALL as a subset

{Y | bigger(Y,X)} C {Y | bigger(Y,X) }

TRUE

QED

Herc