Thread: formalization of sqroot definition

Recently i was asked to formalize the following sqroot definition:

We define the sqroot of a non negative No x ( x>=0),symbolized as sqroot(x), another non negative No y such that when we raise y to the power of two we get x.
Real Nos of course
Although i have an idea your ideas will be appreciated
And then to prove the relevant theorems in a formalized manner

My idea of the formula is the following:

..............(x)(y).[sqroot(x)=y <-----> y^2=x ]

do you agree??

Originally Posted by triclino

Recently i was asked to formalize the following sqroot definition:

We define the sqroot of a non negative No x ( x>=0),symbolized as sqroot(x), another non negative No y such that when we raise y to the power of two we get x.
Real Nos of course
Although i have an idea your ideas will be appreciated
And then to prove the relevant theorems in a formalized manner

To show this is a good definition you need to show such a number y is unique and it exists.

Originally Posted by ThePerfectHacker

To show this is a good definition you need to show such a number y is unique and it exists.

Thank you,

but do we have to do that for every definition??

For example in the definition of the composite function do we have to show that it exists??

In our case the existence has been shown by the following theorem:

.......(x)[ x>=0---------> E!y( y>=0 & y^2=x)].........................

Hence the definition of sqroot(x)

Where E!y means there exists a unique y,and (x) for all x

And now how do we prove :

1) x>=0=======> sqroot(x) >=0

2) x>=0 ======> [sqroot(x)]^2=x

3) sqroot(x^2)= absvalue(x)

4) x>=0 & y>=0=====> sqroot(xy) = sqroot(x)(y)

by using only:............ sqroot(x) = y <------> y^2=x ????....................

thanks