# Formalization of sqroot definition

1. Aug 3, 2008

### peos69

Since in another thread people occupy them selfs with highly formalized formulas let this
thread be the formalization of a high school concept,that of the definition of sqroot.
And then prove all the the theorem concerning sqroots in a formalized manner

2. Aug 3, 2008

### CompuChip

The square root function is the function $\surd: \mathbb{R}_{> 0} \to \mathbb{R}_{> 0}, x \mapsto \sqrt{x}$ satisfying $(\sqrt{x})^2 = x$ and $\sqrt{1} = 1$.​
If you wish you can even define it from all of R to C. Finally you can continue it to all of C but that continuation is not unique.

What theorems would you like to prove?

3. Aug 3, 2008

### peos69

In formalization we do not use words only symbols.
So 1st we define the concept and then we check if it satisfies the definition of a function.So let us formalize it now and then we will prove the theorems.
The definition in words is that given in high school and the field the real Nos field

4. Aug 3, 2008

### peos69

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

5. Aug 3, 2008

### CRGreathouse

For $\mathbb{R}^+\to\mathbb{R}^+:$
$$\sqrt{} :\!= \{(x^2, x)| x\in\mathbb{R}^+\}$$

For $\mathbb{R}\to\mathbb{C}:$
$$\sqrt{} :\!= \{(x^2, x)| x\in\mathbb{R}^+\}\cup\{(-x^2, xi)| x\in\mathbb{R}^+\}\cup\{(0, 0)\}$$

6. Aug 3, 2008

### HallsofIvy

What's wrong with that is that you haven't required that it be continuous. Without that you could have a function for which sqrt(x), for x>= 0 but NOT equal to 1, is negative and sqrt(1)= 1.

With the addition that the function is continuous, that would be perfectly good.

7. Aug 3, 2008

### peos69

Take the high school definition which i gave you above and converted into symbols.
I REAPED:
--------------------------------------------------------------------------------

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 .
Where do you see here functions,sets e.t.c

8. Aug 3, 2008

### CRGreathouse

Formally, a function is a set of ordered pairs.

9. Aug 3, 2008

### peos69

We will come to the formalization of the definition of a function but perhaps in another

10. Aug 3, 2008

### Focus

Its a bit pointless asking people to formalize everything, there is already literature out there on the topic, please read those first. I recommend Principia Matematika by Russel and Whitehead.

11. Aug 3, 2008

### peos69

My friend please tell me have you ever done a single proof in your life in a true formalized
manner????
You know what? A professor in analysis did the same thing.I send him a proof which he could not understand and he started referring me to different books.
But the motivation,as a mention at the beginning of the thread,was not mine. I saw that
GRGREATHOUSE, in another thread,was scrutinizing highly formalized formulas .
But to my surprise here i see that are difficulties in formalizing such a small high school concept like that of sqroot.
Also the formalization of the definition of a function helped me find out things i could not
imagine before hence the spontaneous respond to start a new thread with the formalization of the definition of a function

12. Aug 3, 2008

### Focus

Yes I have done a lot of proofs in a true formalized manner but if you read the book I suggested I'm sure you will find it more than adequate. People are not referring you to books to get rid of you or because they don't understand. There is a reason why those books are out there. Instead of asking people here to formalize things for you just read the book. It takes about 400 pages to get to 2+2=4 I think.

13. Aug 3, 2008

### matheinste

Hello peos69.

I don't have any answers, just a question. What exactly does the word formal mean in this context?

Matheinste.

14. Aug 3, 2008

### peos69

To mention another example take the formalization of the limit of a function a concept very often mentioned in this FORUM .A true formal definition will help you understand the negation of the definition,whilst any other definition will always leave you with a bit of doubt in your mind ,a very lethal stuff in mathematical emancipation.
Further i would like to inform you that in hard analysis very often the negation of a formula help us prove a theorem

15. Aug 3, 2008

### gel

I'm no fan of 'highly formalized' formulas, if that means lots of symbols and no words. But, here you go
$$\forall x\in\mathbb{R}_+\left(\sqrt{x}\in\mathbb{R}_+\wedge(\sqrt{x})^2=x\right).$$

16. Aug 3, 2008

### peos69

My friend you forcing your self to the following demand, i thing by everyone??
Formalize then the definition of the sqroot and then prove arelavent theorem.
Here is your proof that 2+2=4
1st let 0'=1,1'=2,2'=3,3'=4 e.t.c e.t.c
And.........................2+2=2+1'=(2+1)'=(2+0')'=[(2+0)']'= [(2)']'=(3)'=4

17. Aug 3, 2008

### peos69

read the definition in words 1st

18. Aug 3, 2008

### gel

Sorry, I don't follow you. Are you happy with my formalized definition?

19. Aug 3, 2008

### peos69

20. Aug 3, 2008

### Focus

Please don't take my quote out of context, I said the book takes 400 pages to do it. Your proof is incomplete. What is =, what is +, how can you make the step 2+1'=(2+1)' why is 2+0=0. These are only some of the things that you are missing. You choose to assume a lot of things without defining them. You are not even using any axioms like PA or any formal system.

To do logic this say is trivial. It is no more rigorous than assuming 2+2=4. This is why I suggest reading the books first, to give you an idea of how boring long and difficult these things are.
Taking PA and logical relations it is easy to prove a*0=0 or a*(-1)=-a or such, the only problem comes when you have to define equivalence relations, operators, numbers and such. PA is also self referencing with the forth axiom (natural induction), to rid these things are hard.

21. Aug 3, 2008

### peos69

WHERE AM I
THE AXIOMS USED ARE;
for all,x (x+0=x)
for all,x and y ......x+y'=(x+y)'
The Fanny thing is that you suggesting me to read books
+ is a two place operation symbol ,= is a two predicate symbol
IF you want me to give a complete formal proof i can do it the question is can you do it???
But look we are getting out of our subject now ,do you do it on purpose

22. Aug 3, 2008

### peos69

From the formalization of a small concept we landed on formal proofs ,why you doing that because you cannot formalize not even the sqroot concept??

23. Aug 3, 2008

### peos69

Boring ? sure they are particularly if you do not understand them

24. Aug 3, 2008

### peos69

And then people are asking for rigorous proofs.
...................................WHAT IS A RIGOROUS PROOF????

25. Aug 4, 2008

### CompuChip

I gave you a definition, CRGreathouse gave you a more formal definition and gel even gave you one without English words in it. If that's not formal enough for you, I don't think you have the same idea about "formal" as your average mathematician...