Formalization of sqroot definition

  • Context: Undergrad 
  • Thread starter Thread starter peos69
  • Start date Start date
  • Tags Tags
    Definition
Click For Summary

Discussion Overview

The discussion revolves around the formalization of the definition of the square root function, exploring its mathematical properties and theorems related to it. Participants engage in defining the square root in both informal and formal terms, considering its implications in various mathematical contexts.

Discussion Character

  • Exploratory
  • Technical explanation
  • Debate/contested
  • Mathematical reasoning

Main Points Raised

  • Some participants propose defining the square root function as \surd: \mathbb{R}_{> 0} \to \mathbb{R}_{> 0}, satisfying (\sqrt{x})^2 = x and \sqrt{1} = 1.
  • Others suggest that the square root can be defined from all of \mathbb{R} to \mathbb{C}, but note that such a continuation is not unique.
  • A participant emphasizes the need for a formal definition using symbols rather than words, indicating that the definition should be rigorous and satisfy the criteria of a function.
  • Another participant challenges the lack of continuity in some proposed definitions, arguing that without continuity, the square root function could yield negative values for inputs other than 1.
  • Some participants express frustration with the difficulty of formalizing what they consider a basic high school concept, questioning the need for extensive formalization.
  • There are discussions about the nature of formal definitions and the importance of understanding the negation of definitions in mathematical reasoning.
  • One participant shares a formalized definition using logical quantifiers, while another critiques the completeness of a proof presented in the discussion.

Areas of Agreement / Disagreement

Participants do not reach a consensus on the formalization of the square root definition. Multiple competing views and definitions are presented, with some participants advocating for a more rigorous approach while others question the necessity of such formalism.

Contextual Notes

Limitations include varying interpretations of what constitutes a formal definition, the dependence on specific mathematical frameworks, and unresolved discussions about continuity and completeness in definitions and proofs.

Who May Find This Useful

This discussion may be of interest to those studying mathematical formalism, particularly in the context of real analysis and the foundations of mathematics.

  • #31
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)
 
Mathematics news on Phys.org
  • #32
peos69 said:
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.

peos69 said:
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.
 
  • #33
I don't think it's wise to get caught up in this never-ending cycle, but still I'm going to do it :smile:

CompuChip said:
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
 
  • #34
CompuChip said:
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
 
  • #35
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 :smile: And I didn't even notice... need to get some sleep)
 
  • #36
SO NOW YOU found out that your definition WAS INCOMPLETE.
I wonder WHAT NEXT
 
  • #37
peos69 said:
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!
 
  • #38
focus said:
the Theorem Does Not Hold For All X!

As I Said What Next
 
  • #39
But i am sorry we Curry on tomorrow
 
  • #40
peos69 said:
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.
 
  • #41
Focus said:
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
 
  • #42
\sqrt{} :\!= \{(x^2, x)| x\in\mathbb{R}^+\}\cup\{(-x^2, xi)| x\in\mathbb{R}^+\}\cup\{(0, 0)\}

peos69 said:
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.
 
  • #43
peos69 said:
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 x2>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).
 
Last edited:
  • #44
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
 
  • #45
gel said:
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 x2>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
 
  • #46
SORRY gel I THOGHT you were Focus
 
  • #47
\sqrt{} :\!= \{(x^2, x)| x\in\mathbb{R}^+\}\cup\{(-x^2, xi)| x\in\mathbb{R}^+\}\cup\{(0, 0)\}

peos69 said:
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.
 
  • #48
Wonder how we managed before peos69 showed up to teach us all how to do maths.
 
  • #49
gel said:
Wonder how we managed before peos69 showed up to teach us all how to do maths.

Amen
 
  • #50
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
 
  • #51
Focus said:
2) Which definition to use?

.

Your definition of course
 
  • #52
peos69 said:
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...

peos69 said:
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.

peos69 said:
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|.

peos69 said:
IF YOU CANNOT prove a theorem it does not mean it is not correct
Who said otherwise?

peos69 said:
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.

peos69 said:
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.
 
  • #53
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).
 
  • #54
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??
 
  • #55
Sorry i should have said ,wrong set theory instead of only set theory
 
  • #56
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.
 
  • #57
CompuChip said:
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?
 
  • #58
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 definition 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|
 
Last edited:
  • #59
uman said:
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
 
  • #60
arildno said:
What is the problem here?
Peos69. Otherwise, none.
 

Similar threads

  • · Replies 5 ·
Replies
5
Views
3K
  • · Replies 0 ·
Replies
0
Views
1K
  • · Replies 23 ·
Replies
23
Views
2K
  • · Replies 3 ·
Replies
3
Views
2K
  • · Replies 40 ·
2
Replies
40
Views
8K
  • · Replies 13 ·
Replies
13
Views
3K
  • · Replies 2 ·
Replies
2
Views
2K
  • · Replies 1 ·
Replies
1
Views
2K
  • · Replies 5 ·
Replies
5
Views
2K
  • · Replies 25 ·
Replies
25
Views
4K