Formalization of sqroot definition

[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):
$(\sqrt{x}\sqrt{y})^2=(\sqrt{x})^2(\sqrt{y})^2=xy=(\sqrt{xy})^2$.
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):
$(\sqrt{x}\sqrt{y})^2=(\sqrt{x})^2(\sqrt{y})^2=xy=(\sqrt{xy})^2$.
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

 

[peos69]

2) Which definition to use?

.

Your definition of course

 

[CompuChip]

CONGRATULATIONS YOU DECIDED to learn the famous step wise semi formal proof, i wonder who was the inventor of that proof.

You mean who was the one that gave it first? I don't think for such trivial theorems this is relevant...

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.

In logic, "for all x" means: "for all x in the universe of discourse." If the square root is only defined for positive x, you can only prove things about it for positive 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)

You should be clear about your notation.
$$( \sqrt{-3} )^2 = -3 \stackrel{!}{\neq} \sqrt{(-3)^2} = 3$$.
This is even more easy to prove, as: (Let x > 0):
$$(-x)^2 = x^2$$ so $$\sqrt{(-x)^2} = \sqrt{x^2} = x$$ (I'm "guessing" a root here and by injectivity properties it is the unique one). And by the way absolute value works, x = |-x|.

IF YOU CANNOT prove a theorem it does not mean it is not correct

Who said otherwise?

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

Actually my definition was perfectly correct. Especially since you keep stressing "high school"... I don't know about you but I didn't learn about complex numbers until after high school, so the definition on $\mathbb{R}_+$ is perfectly all right. Also the proof I gave was perfectly correct and the theorem was true as well. But then you started about x < 0, so I extended (not: completely changed!) the definition and showed that the theorem was wrong and proved the correct version of it.

OF COURSE your definition of sq root is pathetic let alone wrong. [...] 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
[...]

I think I'm done in this thread, I'll see you when you've decided to do real mathematics.

 

[uman]

Theorem. The set of all nonnegative real numbers whose square is less than some positive real number a has a supremum.
Proof.
If a>=1, x^2 < a implies x < a < a+1, since x^2<1 if x<1 and x < x^2 if x > 1.
If a<1, x^2 < a implies x < 1 < a+1. In either case, the set in question is bounded above by a+1. Since 0 is in the set, it is nonempty and therefore has a supremum by the least upper bound axiom.

Notation. Let R* be the set of nonnegative real numbers.

Definition. Let the "square root function" be the relation f: R* -> R* defined as follows:
1) (0,0) is in f.
2) If x > 0, let y denote the supremum of the set of nonnegative real numbers whose square is less than x. Then (x,y) is in f.
3) No other ordered pair is in f.

Theorem. f is a function.
Proof.
If (0,a) is in f, 1), 2), and 3) together show that a must equal 0.
If (x,a) is in f and x != 0, 3) and 2), as well as the fact that the supremum of a set of real numbers is unique when it exists, show that a is uniquely determined by x.
If x is a real number greater than or equal to zero, (x,a) is in f for some a.
The first two statements show that f is defined everywhere on its domain, and the last shows that the value of f(x) is uniquely determined. Hence x is a function.

Theorem. f(x^2) = abs(x).
Proof. Assume x is positive. Then f(x^2) is the supremum of the set of real numbers y such that y^2 < x^2. If f(x^2) > x, let a = (f(x^2) + x)/2 < f(x^2). Since f(x^2) is the supremum of the set of real numbers y such that y^2 < x^2, we should have a^2 < x^2. But a > x, so a^2 > x^2. It is similarly easy to prove that f(x^2) is not less than x, so f(x^2) = x = abs(x).

Assume x is negative. Then (-x) is positive, and (-x)^2 = x^2. We may apply the statement just proven to obtain f(x^2) = f((-x)^2) = abs(-x) = abs(x).

f(0) = 0 = abs(0), by the definition of f.

These three statements together show that f(x^2) = abs(x).

 

[peos69]

If somebody asks you to teach him how to drive a car you put in an airspace bus and you send him to the moon, or if a kid ask you to teach him how to count you do it thru
set theory??

 

[peos69]

Sorry i should have said ,wrong set theory instead of only set theory

 

[CompuChip]

Peos you seem to be convinced that you are right and all of us are wrong. Unless you can clearly explain your problem instead of repeating that our mathematics is not right, I don't think anyone can help you.

 

[Gokul43201]

Unless you can clearly explain your problem ...

After all this, you want to give peos another chance? What if you find out that peos made another unacknowledged notation error 3 pages too late? Why waste your time?

 

[arildno]

What is the problem here?
Let us take the high-school "definition" of the sqrt of a non-negative number "a" as the non-negative number that multiplied with itself equals a, i.e:
$$\sqrt{a}*\sqrt{a}=a$$
Or, equivalently:
$$(\sqrt{a})^{2}=a$$
As for proving $$\sqrt{a^{2}}=|a|$$
we note that $\sqrt{a^{2}}$ must satisfy the equation:
$$x^{2}=a^{2}$$
From this equation, it follows that either x=a, OR, x=-a.
But in our defintion of the square root, we required that it has to be the NON-negative number with that property!
Thus, it follows that x=a IF a>=0, and x=-a IF a<0.
But this is precisely what is encapsulated in the concept of the "absolute value" of a number, hence we have proven that:
$$\sqrt{a^{2}}=|a|$$

 

[peos69]

Assume x is negative. Then (-x) is positive, and (-x)^2 = x^2. We may apply the statement just proven to obtain f(x^2) = f((-x)^2) = abs(-x) = abs(x).

f(0) = 0 = abs(0), by the definition of f.

These three statements together show that f(x^2) = abs(x).

WHEN X<0 THEN abs(x)=-x AND NOT abs(x) = x
LEARN THE DEFINITION of the absolute value of a REAL No

 

[CompuChip]

What is the problem here?

Peos69. Otherwise, none.

 

[CRGreathouse]

Assume x is negative. Then (-x) is positive, and (-x)^2 = x^2. We may apply the statement just proven to obtain f(x^2) = f((-x)^2) = abs(-x) = abs(x).

f(0) = 0 = abs(0), by the definition of f.

These three statements together show that f(x^2) = abs(x).

WHEN X<0 THEN abs(x)=-x AND NOT abs(x) = x
LEARN THE DEFINITION of the absolute value of a REAL No

uman didn't claim that abs(x) = x for x negative, just that abs(-x) = abs(x).

 

[peos69]

arildo your proof is right but where is the formalization of the definition??
Now we started getting somewhere

 

[peos69]

uman didn't claim that abs(x) = x for x negative, just that abs(-x) = abs(x).

HE DID the fatal mistake to use a formula which he proved ONLY FOR X>=0
definitely his formula does not apply for x<0,unless he proves (assuming he proves),
that f(x^2)= -x

 

[peos69]

After all this, you want to give peos another chance? What if you find out that peos made another unacknowledged notation error 3 pages too late? Why waste your time?

HOW MANY have i done up to now??
NAME them

 

[peos69]

Peos you seem to be convinced that you are right and all of us are wrong. Unless you can clearly explain your problem instead of repeating that our mathematics is not right, I don't think anyone can help you.

Definitely i have no problem the problem is yours that you cannot give a proper formalization of a h.school concept
You must also remember i did not discovered the sqroot

 

[arildno]

arildo your proof is right but where is the formalization of the definition??
Now we started getting somewhere

What nonsense are you talking?
My definition is perfectly formalized, in that particular format known as plain, English language.

 

[Gokul43201]

HOW MANY have i done up to now??
NAME them

Try these for size:

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

And several posts later...

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

Both have parentheses in the wrong place. This was pointed out more than once, and you've chosen not to acknowledge it.

And quit with the capitals already, if you don't wish to get booted from here.

 

[peos69]

What nonsense are you talking?
My definition is perfectly formalized, in that particular format known as plain, English language.

FORMALIZATION IS FREE from any language that's the beauty of it

 

[arildno]

FORMALIZATION IS FREE from any language that's the beauty of it

Nonsense.
Besides, I note that you didn't bother to heed Gokul's WARNING.

 

[HallsofIvy]

I suspect that one problem is that after 68 posts in this thread you have never said exactly what you mean by "formalization".