Formalization of sqroot definition

[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

 

[CompuChip]

What about this definition:

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?

 

[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

 

[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

 

[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)\}

 

[HallsofIvy]

What about this definition:

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?

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.

 

[peos69]

ALL I asked is:
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

 

[CRGreathouse]

Where do you see here functions,sets e.t.c

Formally, a function is a set of ordered pairs.

 

[peos69]

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

 

[Focus]

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

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.

 

[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

 

[Focus]

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

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.

 

[matheinste]

Hello peos69.

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

Matheinste.

 

[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

 

[gel]

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

 

[peos69]

Yes I have done a lot of proofs in a true formalized manner . It takes about 400 pages to get to 2+2=4 I think.

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

 

[peos69]

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

read the definition in words 1st

 

[gel]

read the definition in words 1st

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

 

[peos69]

Please let me answer to your question a Little bit latter

 

[Focus]

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

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.

 

[peos69]

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.

.

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

 

[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??

 

[peos69]

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.
.

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

 

[peos69]

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

 

[CompuChip]

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??

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...

 

[Focus]

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...

To be honest this isn't logic. It's analysis. I prefer to define the square root as
\sqrt{x}=sup\{a|a\in\mathbb{R},a^2&lt;x\} for x\in\mathbb{R}_+
The superemum exists by completeness of R.

peos69, if you think you can derive 2+2=4 in less than 400 pages with defining everything you use on the way, then be my guest. And please don't post things like this here. This is all analysis and in no way logic.

 

[peos69]

Is that the definition of the sqroot that your teacher taught you when you were in high school?
In maths we swim in the sea of logic all the time,analysis too

 

[peos69]

But before i give you a formal proof of 2+2=4,please give me YOUR definition of formal
proof so that i will know how to act.
And of course we will do it latter.

 

[Focus]

Is that the definition of the sqroot that your teacher taught you when you were in high school?
In maths we swim in the sea of logic all the time,analysis too

It doesn't matter what my high school teacher taught me. My definition of a square root is perfectly well defined. You can use to prove facts about square roots. Just because we swim in a sea of logic does not mean it is logic. This thread is analysis and not logic. Logic does not concern itself with defining things on a set of axioms.

But before i give you a formal proof of 2+2=4,please give me YOUR definition of formal
proof so that i will know how to act.
And of course we will do it latter.

I want you to define everything you use i.e. set out a minimum set of axioms and prove that 2+2=4. Your axioms should not be inconsistent or restrictive. I can prove 2+2=4 by simply saying my axiom is PA or an axiom saying 2+2=4. I want you to define a formal system you are working in and all the interference rules. Define variables, quantifiers etc..


First you should probably read about logic instead of mistaking other fields of maths to be logic.

 

[peos69]

1)THIS THREAD was intended to formalize a h.school definition and NOT i repeat NOT for everyone to give his own definition of sqroot,right or wrong.What is the mater with you guys can't we communicate?
2)Imagine Focus you give your h.school pupils a definition of the short you mention,WHAT WILL happen?MUST THEY learn ANALYSIS BEFORE h.school Algebra?

 

[peos69]

ok you guys, go ahead and proove with your definitons the following h.school theorems.
1)for all x sqoot (x)^2 = absolute value (x)
2)for x >=0 and y>=0 then sqroot(xy)=sqroot(x)*sqroot(y)

 

[Focus]

1)THIS THREAD was intended to formalize a h.school definition and NOT i repeat NOT for everyone to give his own definition of sqroot,right or wrong.What is the mater with you guys can't we communicate?
2)Imagine Focus you give your h.school pupils a definition of the short you mention,WHAT WILL happen?MUST THEY learn ANALYSIS BEFORE h.school Algebra?

1) There are more than one way of defining things. You can prove most definitions are equivalent. Some are better at proving some theorems than others.

2) I don't really care if high school kids understand it or not. If you want to formalize something you can't do it at a high school knowledge. If you want to teach this at high schools either teach them set theory first or don't bother formalizing.

ok you guys, go ahead and proove with your definitons the following h.school theorems.
1)for all x sqoot (x)^2 = absolute value (x)
2)for x >=0 and y>=0 then sqroot(xy)=sqroot(x)*sqroot(y)

1) Is not a true statement take (\sqrt{-1})^2=-1\neq 1
2) Which definition to use?

Again this isn't logic, its analysis.

 

[CompuChip]

I don't think it's wise to get caught up in this never-ending cycle, but still I'm going to do it

What about this definition:

The square root function is the continuous function \surd: \mathbb{R}_+ \to \mathbb{R}_+, x \mapsto \sqrt{x} satisfying (\sqrt{x})^2 = x and \sqrt{1} = 1.​

(Thank you Halls, I added the continuity. Also thank you to the one who used the \mathbb{R}_+ notation, I like it better

Theorem 1: for all x sqoot (x)^2 = absolute value (x)

Proof: Let x \in \mathbb{R}^+. Then by definition (\sqrt{x})^2 = x and because x > 0, x = |x|. QED

Theorem 2: for x >=0 and y>=0 then sqroot(xy)=sqroot(x)*sqroot(y)

Proof: The quadratic function x \mapsto x^2 is injective on \mathbb{R}_+ so it follows from ( \sqrt{x} \sqrt{y} )^2 = (\sqrt{x y})^2 and (ab)^2 = a^2 b^2 for all real positive a, b. QED

 

[peos69]

I :




Theorem 1: for all x sqoot (x)^2 = absolute value (x)

Proof: Let x \in \mathbb{R}^+. Then by definition (\sqrt{x})^2 = x and because x > 0, x = |x|. QED

. QED

Lets take things step by step:
The theorem is FOR ALL X AND NOT ONLY for x>=0 so now try to prove for ....x<0

 

[CompuChip]

I only defined it for x > 0. But if you extend the definition by
\sqrt{-x} := i \sqrt{x} for x > 0 where i satisfies i^2 = -1 by definition, then
(\sqrt{-x}\right)^2 = (i \sqrt{x})^2 = -x
by the part already proven.

(So the theorem was wrong And I didn't even notice... need to get some sleep)

 

[peos69]

SO NOW YOU found out that your definition WAS INCOMPLETE.
I wonder WHAT NEXT

 

[Focus]

Lets take things step by step:
The theorem is FOR ALL X AND NOT ONLY for x>=0 so now try to prove for ....x<0

The theorem does not hold for all x!

 

[peos69]

the Theorem Does Not Hold For All X!

As I Said What Next

 

[peos69]

But i am sorry we Curry on tomorrow

 

[Focus]

As I Said What Next

Make a theorem that is actually correct. I gave a counter example to what you are asking to prove. If the theorem is not correct then there will almost surely be no proof.

 

[peos69]

The theorem does not hold for all x!

NEARLY EVERY h.school textbook and indeed in the lower classes proves that theorem,would you care to look,there it says for all x.
But let us see if the theorem holds for x<0.
let x=-3 then sq root(-3)^2=sq root(9)=3.
Also abs value(-3)=3
Hence sq root(x)^2= abs value(x)
IF YOU CANNOT prove a theorem it does not mean it is not correct

 

[CRGreathouse]

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

ok you guys, go ahead and proove with your definitons the following h.school theorems.
1)for all x sqoot (x)^2 = absolute value (x)
2)for x >=0 and y>=0 then sqroot(xy)=sqroot(x)*sqroot(y)

With my definition (above), #1 does not hold, at least for the usual meaning of absolute value. For example, (-1, i)\in\sqrt{} but \sqrt{-1}^2=-1\neq|-1|.

I would formalize #2 as follows:

Suppose x,y\ge0.

1. x-0\in\mathbb{R}^+\vee x^2=0 (definition of \ge).
2. x\in\mathbb{R}^+\vee x^2=0 (additive identity).
3. x\in\mathbb{R}^+\to(x^2,x)\in\sqrt{} (definition of square root)
4. x=0\to(x^2,x)\in\sqrt{} (definition of square root)
5. (x^2,x)\in\sqrt{} (disjunctive inference)
6-10. (y^2,y)\in\sqrt{} (as 1-5, but with y instead of x)
11. x^2=0\to\sqrt{x^2y^2}=\sqrt{0^2y^2}=\sqrt{0y^2}=\sqrt{0}=0 (substitution, multiplication, zero property of multiplication, uniqueness of square roots)
12. x^2=0\to\sqrt{x^2}\sqrt{y^2}=\sqrt{0^2}\sqrt{y^2}=\sqrt{0}\sqrt{y^2}=0\sqrt{y^2}=0 (substitution, multiplication, zero property of multiplication)
13. x^2=0\to\sqrt{x^2y^2}=0\wedge\sqrt{x^2}\sqrt{y^2}=0 (conjunctive inference)
14. x^2=0\to\sqrt{x^2y^2}=\sqrt{x^2}\sqrt{y^2} (substitution)
15-18. x^2=0\to\sqrt{x^2y^2}=\sqrt{x^2}\sqrt{y^2} (same as 11-14, but reversing x and y and using right-handed zero property instead of left-handed)
19. x^2\in\mathbb{R}^+\wedge y^2\in\mathbb{R}^+\to x^2y^2\in\mathbb{R}^+ (closure of positive reals under *)

Okay, this is getting boring. This proof would take at least ten more steps. And frankly, this proof assumes (by its form) that positive real numbers have square roots, and explicitly assumes the uniqueness of square roots and closure under *. These would add at least fifty more steps -- and probably not that few -- if they were proved as well from first principles.

 

[gel]

let x=-3 then sq root(-3)^2=sq root(9)=3.

I think your notation caused some confusion here. You asked for \sqrt{(-3)^2} but the way you have the bracket it looks like (\sqrt{-3})^2. It's also not clear what you are meant to assume before proving the results you ask. I'll assume that that R is an ordered field and sqrt(x) exists for x>=0.

The theorems you want would be easier if you first showed that
(0) x^2=y^2\,\Rightarrow\,x=y for x,y>=0.
This follows from factorizing (x+y)(x-y)=0, in which case x=y or x=-y. As x,y>=0, the second case is only true if x=y=0, so, in either case you have x=y.

To prove (1):
For x>= 0, (\sqrt{x^2})^2=x^2 by definition, so applying (0), \sqrt{x^2}=x=|x|.
If x<0 you have -x>0 and x²>0, and \sqrt{x^2}=\sqrt{(-x)^2}=-x=|x|.

To prove (2):
<br /> (\sqrt{x}\sqrt{y})^2=(\sqrt{x})^2(\sqrt{y})^2=xy=(\sqrt{xy})^2<br />.
The result follows by applying (0).

Not as formal as CRGreathouse's reply, I'll admit. But I don't have the energy or time for that (and can't remember the last time I used words such as conjunctive inference).

 

[peos69]

CONGRATULATIONS YOU DECIDED to learn the famous step wise semi formal proof, i wonder who was the inventor of that proof.
Good for you from now on you will have the power to get into everything and Analise it .
OF COURSE your definition of sq root is pathetic let alone wrong.
THE ART of formalizing is one think and the art of a formal proof another,to get things right it will take you a lot of sleepless nights.
A well written semi formal poof is never boring,thats a word used by those that they cannot do it
IN TOUGH analysis where a lot of theorems are incomplete ,wrong or at least badly written this kind of proof will get you on top of things.
Finally in what is coming you will see that the proof of those theorems are just a few lines in a formalized manner and not of course in a semi formal proof which we can do if there is a demand for it

 

[peos69]

I think your notation caused some confusion here. You asked for \sqrt{(-3)^2} but the way you have the bracket it looks like (\sqrt{-3})^2. It's also not clear what you are meant to assume before proving the results you ask. I'll assume that that R is an ordered field and sqrt(x) exists for x>=0.

The theorems you want would be easier if you first showed that
(0) x^2=y^2\,\Rightarrow\,x=y for x,y>=0.
This follows from factorizing (x+y)(x-y)=0, in which case x=y or x=-y. As x,y>=0, the second case is only true if x=y=0, so, in either case you have x=y.

To prove (1):
For x>= 0, (\sqrt{x^2})^2=x^2 by definition, so applying (0), \sqrt{x^2}=x=|x|.
If x<0 you have -x>0 and x²>0, and \sqrt{x^2}=\sqrt{(-x)^2}=-x=|x|.

To prove (2):
<br /> (\sqrt{x}\sqrt{y})^2=(\sqrt{x})^2(\sqrt{y})^2=xy=(\sqrt{xy})^2<br />.
The result follows by applying (0).

Not as formal as CRGreathouse's reply, I'll admit. But I don't have the energy or time for that (and can't remember the last time I used words such as conjunctive inference).

SO NOW YOU DECIDED the theorem is for all X
A man that changes his mind so quickly is not called a mathematician but a politician

 

[peos69]

SORRY gel I THOGHT you were Focus

 

[CRGreathouse]

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

ok you guys, go ahead and proove with your definitons the following h.school theorems.
1)for all x sqoot (x)^2 = absolute value (x)
2)for x >=0 and y>=0 then sqroot(xy)=sqroot(x)*sqroot(y)

With my definition (above), #1 does not hold, at least for the usual meaning of absolute value. For example, (-1, i)\in\sqrt{} but \sqrt{-1}^2=-1\neq|-1|.

I would formalize #2 as follows:

Suppose x,y\ge0.

1. x-0\in\mathbb{R}^+\vee x^2=0 (definition of \ge).
2. x\in\mathbb{R}^+\vee x^2=0 (additive identity).
3. x\in\mathbb{R}^+\to(x^2,x)\in\sqrt{} (definition of square root)
4. x=0\to(x^2,x)\in\sqrt{} (definition of square root)
5. (x^2,x)\in\sqrt{} (disjunctive inference)
6-10. (y^2,y)\in\sqrt{} (as 1-5, but with y instead of x)
11. x^2=0\to\sqrt{x^2y^2}=\sqrt{0^2y^2}=\sqrt{0y^2}=\sqrt{0}=0 (substitution, multiplication, zero property of multiplication, uniqueness of square roots)
12. x^2=0\to\sqrt{x^2}\sqrt{y^2}=\sqrt{0^2}\sqrt{y^2}=\sqrt{0}\sqrt{y^2}=0\sqrt{y^2}=0 (substitution, multiplication, zero property of multiplication)
13. x^2=0\to\sqrt{x^2y^2}=0\wedge\sqrt{x^2}\sqrt{y^2}=0 (conjunctive inference)
14. x^2=0\to\sqrt{x^2y^2}=\sqrt{x^2}\sqrt{y^2} (substitution)
15-18. x^2=0\to\sqrt{x^2y^2}=\sqrt{x^2}\sqrt{y^2} (same as 11-14, but reversing x and y and using right-handed zero property instead of left-handed)
19. x^2\in\mathbb{R}^+\wedge y^2\in\mathbb{R}^+\to x^2y^2\in\mathbb{R}^+ (closure of positive reals under *)

Okay, this is getting boring. This proof would take at least ten more steps. And frankly, this proof assumes (by its form) that positive real numbers have square roots, and explicitly assumes the uniqueness of square roots and closure under *. These would add at least fifty more steps -- and probably not that few -- if they were proved as well from first principles.

 

[gel]

Wonder how we managed before peos69 showed up to teach us all how to do maths.

 

[Focus]

Wonder how we managed before peos69 showed up to teach us all how to do maths.

Amen

 

[peos69]

Some times we take minor things for granted,they lay there,we use them in our every day life.
For example if some body asks you what is the sq root of 9 you will all automatically say 3, but look what happens when you asked for the definition.
Take another example.EVERY one is acquainted with the word argument we use the word every day,but if you ask for a definition everyone apart from the experts will give you a wrong definition.TRY IT.
CONSIDERING i have already asked couple of professors and they did not know 100%,you doing fine