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