My idea of the formula is the following:
..............(x)(y).[sqroot(x)=y <-----> y^2=x ]
do you agree??
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
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