Prove a|x|+bx ≥ 0 $\Rightarrow$ a ≥ |b|

  • MHB
  • Thread starter solakis1
  • Start date
  • Tags
    Proof
In summary: So it's conceivable that someone could confirm the correctness of the proof using a computer program. But of course, it would be an interesting challenge.
  • #1
solakis1
422
0
In a high school book i found the following problem with its proof.

Problem:

Prove that : if ,for all,x $ a|x|+bx\geq 0$ then $ a\geq |b|$

Proof:

Suppose that for each x we have $a|x|+bx\geq 0$.............1
we must show that : $a\geq |b|$

Because (1) holds for each x it will hold and for x=1 and x=-1.

From (1) for x=1 we have that $a+b\geq 0$ or $a\geq -b$,while for x=-1 that $a-b\geq 0$ or $a\geq b$.Hence we have $a\geq -b$ and $a\geq b$ or $a\geq |b|$.

Is that proof correct??
 
Physics news on Phys.org
  • #2
solakis said:
Is that proof correct??
Yes.
 
  • #3
Evgeny.Makarov said:
Yes.

Can you have : x=1 and x=-1 ??
 
  • #4
solakis said:
Can you have : x=1 and x=-1 ??

Well, certainly not at the same time and in the same respect. That is, you can't have $x=1$ AND $x=-1$. But you could have $x=1$ OR $x=-1$. And since the given relation holds for all $x$, it holds if you first consider $x=1$, and then consider $x=-1$ as they do in the proof.
 
  • #5
Ackbach said:
Well, certainly not at the same time and in the same respect. That is, you can't have $x=1$ AND $x=-1$. But you could have $x=1$ OR $x=-1$. And since the given relation holds for all $x$, it holds if you first consider $x=1$, and then consider $x=-1$ as they do in the proof.
In that case you do not have : $ a\geq -b$ AND $ a\geq b$ as they consider in the proof ,

But : $ a\geq -b$ OR $ a\geq b$
 
  • #6
solakis said:
In that case you do not have : $ a\geq -b$ AND $ a\geq b$ as they consider in the proof ,

But : $ a\geq -b$ OR $ a\geq b$

Well, I'm not sure I would agree. I think it's more subtle than that. Perhaps my previous post was a bit misleading. I was trying to avoid a situation where you could claim that $1=-1$.

When you say that something is true for all $x$ in a set, you're saying it's true for any particular value of $x$ in the set, including several values chosen one at a time. Moreover, once you've chosen a particular $x$ and plugged it into the original inequality, you have a true statement and the $x$ "drops out". That is, the setup of the problem gives you a schema for generating true statements, all of which are true simultaneously, and none of which contain $x$. $x$ is allowed to range over the whole set.

This is the meaning of the "for all" quantifier.
 
  • #7
Ackbach said:
Well, I'm not sure I would agree. I think it's more subtle than that. Perhaps my previous post was a bit misleading. I was trying to avoid a situation where you could claim that $1=-1$.

When you say that something is true for all $x$ in a set, you're saying it's true for any particular value of $x$ in the set, including several values chosen one at a time. Moreover, once you've chosen a particular $x$ and plugged it into the original inequality, you have a true statement and the $x$ "drops out". That is, the setup of the problem gives you a schema for generating true statements, all of which are true simultaneously, and none of which contain $x$. $x$ is allowed to range over the whole set.

This is the meaning of the "for all" quantifier.

Well ,i hoping that Makarov thru a computer program could give us an exact answer whether the above proof is correct or not
 
  • #8
solakis said:
Well ,i hoping that Makarov thru a computer program could give us an exact answer whether the above proof is correct or not
And who will prove the program correct?

CB
 
  • #9
solakis said:
Well ,i hoping that Makarov thru a computer program could give us an exact answer whether the above proof is correct or not
I formalized the proof. It uses several lemmas:

Code:
forall x : R, Rabs (- x) = Rabs x
Rabs 1 = 1
forall r1 r2 : R, r1 * - r2 = - (r1 * r2)
forall r : R, r * 1 = r
forall x a : R, x <= a -> - a <= x -> Rabs x <= a.

plus some decision procedure for linear inequalities.

As Ackbach explained, the rule of universal quantifier elimination, or universal instantiation, allows deriving from ∀x. P(x) any number of instances P(t) for any expression t. This does not mean that x becomes equal to different expressions t1, t2, ... simultaneously.
 
  • #10
CaptainBlack said:
And who will prove the program correct?
Obviously, there is never full certainty. Sometimes I wonder if I can be sure that I read and copied something correctly even though I don't have dyslexia. If I remember correctly, there was a discussion about this in the science fiction novel Solaris by Stanisław Lem where the protagonist was wondering if he went crazy and can trust the reading of instruments on a spaceship. He ended up performing a complicated computation on the computer that got confirmed by an experiment (or was it? I don't remember very well), so he knew that what he saw was not a hallucination because his brain would not be able to perform such computation.

Some proof assistants have a so-called kernel where the rules of mathematical reasoning are programmed. Ideally, the number of such rules is quite small. The rules of type theory (an extension of lambda calculus) can be written on one page. In a real proof assistant they may be more complicated, but hopefully it's not hundreds of pages. Then all reasoning that the proof assistant verifies gets channeled through this kernel. This is called de Bruijn principle.

A proof assistant can have a lot of facilities built on top of the kernel: means of syntax extension, decision procedures for certain class of formulas, ways of guessing implied parameters (e.g., we often refer to the field of reals just by mentioning the carrier, and the operations and axioms are implied) and so on. But everything is broken down and eventually fed through the kernel. If the kernel says OK, the proof step is accepted. If there is an error either during the breaking down stage or in the kernel itself, the step is rejected. Therefore you know that as long as the kernel is correct, the proof is sound.

By design, people try to make kernels small. In HOL Light, for example, it consists of fewer than 500 lines of computer code, so it is realistic to examine it manually or even formalize in some other proof assistant. Besides, the idea of formal methods is that the rules programmed into the kernel are not just invented for convenience, but form a nice mathematical object (such as Zermelo–Fraenkel set theory). This object is also extensively studied in mathematics to make sure that it does not give rise to contradictions.

I highly recommend a special issue on formal proof of the Notices of the American Mathematical Society (Volume 55, Number 11). Here is a quotation by Thomas Hales from the first article.

Experience from other top-tier theorem-proving
systems has been that about three to five bugs
have been found in each system over a period of
15-20 years of use. After decades of use on many
different systems, to my knowledge, only one proof
has ever had to be retracted as a result of a bug in a
theorem-proving system, and this in a system that I
do not rank in the top-tier: in 1995 a heap overflow
error led to the false claim that the theorem-prover
REVEAL had solved the Robbins conjecture. We can
assert with utmost confidence that the error rates
of top-tier theorem-proving systems are orders
of magnitude lower than error rates in the most
prestigious mathematical journals. Indeed, since a
formal proof starts with a traditional proof, then
does strictly more checking even at the human
level, it would be hard for the outcome to be
otherwise.
 
  • #11
Evgeny.Makarov said:
I formalized the proof. It uses several lemmas:

Code:
forall x : R, Rabs (- x) = Rabs x
Rabs 1 = 1
forall r1 r2 : R, r1 * - r2 = - (r1 * r2)
forall r : R, r * 1 = r
forall x a : R, x <= a -> - a <= x -> Rabs x <= a.

plus some decision procedure for linear inequalities.

As Ackbach explained, the rule of universal quantifier elimination, or universal instantiation, allows deriving from ∀x. P(x) any number of instances P(t) for any expression t. This does not mean that x becomes equal to different expressions t1, t2, ... simultaneously.

Meaning that the proof is correct??
 
  • #12
solakis said:
Meaning that the proof is correct??
Evgeny.Makarov said:
Yes.
...
 
  • #13
Evgeny.Makarov said:
Obviously, there is never full certainty. Sometimes I wonder if I can be sure that I read and copied something correctly even though I don't have dyslexia. If I remember correctly, there was a discussion about this in the science fiction novel Solaris by Stanisław Lem where the protagonist was wondering if he went crazy and can trust the reading of instruments on a spaceship. He ended up performing a complicated computation on the computer that got confirmed by an experiment (or was it? I don't remember very well), so he knew that what he saw was not a hallucination because his brain would not be able to perform such computation.

Some proof assistants have a so-called kernel where the rules of mathematical reasoning are programmed. Ideally, the number of such rules is quite small. The rules of type theory (an extension of lambda calculus) can be written on one page. In a real proof assistant they may be more complicated, but hopefully it's not hundreds of pages. Then all reasoning that the proof assistant verifies gets channeled through this kernel. This is called de Bruijn principle.

A proof assistant can have a lot of facilities built on top of the kernel: means of syntax extension, decision procedures for certain class of formulas, ways of guessing implied parameters (e.g., we often refer to the field of reals just by mentioning the carrier, and the operations and axioms are implied) and so on. But everything is broken down and eventually fed through the kernel. If the kernel says OK, the proof step is accepted. If there is an error either during the breaking down stage or in the kernel itself, the step is rejected. Therefore you know that as long as the kernel is correct, the proof is sound.

By design, people try to make kernels small. In HOL Light, for example, it consists of fewer than 500 lines of computer code, so it is realistic to examine it manually or even formalize in some other proof assistant. Besides, the idea of formal methods is that the rules programmed into the kernel are not just invented for convenience, but form a nice mathematical object (such as Zermelo–Fraenkel set theory). This object is also extensively studied in mathematics to make sure that it does not give rise to contradictions.

I highly recommend a special issue on formal proof of the Notices of the American Mathematical Society (Volume 55, Number 11). Here is a quotation by Thomas Hales from the first article.

Even if that all works OK (and I am pretty sure that the probability of it being error free is as close to zero as I can imagine) you have the problem of proving the compiler/interpreter is correct, and even then you need to prove that the hardware is correct. (I will let you off the need to screen the system from cosmic rays since you can run it three times to detect errors at to a reasonable level of confidence, but even then we are still dealing with it probably being correct, so maybe we do need to screen it from cosmic rays after all).

That still leaves us with other random errors.

At the end of all this we may be more confident than if we check the proof by hand, but we are qualitivly in the same position, the proof is probably correct.

Anyway, this is all academic, since I do not believe in the enterprise anyway.

CB
 
  • #14
CaptainBlack said:
Even if that all works OK (and I am pretty sure that the probability of it being error free is as close to zero as I can imagine) you have the problem of proving the compiler/interpreter is correct, and even then you need to prove that the hardware is correct. (I will let you off the need to screen the system from cosmic rays since you can run it three times to detect errors at to a reasonable level of confidence, but even then we are still dealing with it probably being correct, so maybe we do need to screen it from cosmic rays after all).

That still leaves us with other random errors.

At the end of all this we may be more confident than if we check the proof by hand, but we are qualitivly in the same position, the proof is probably correct.

Anyway, this is all academic, since I do not believe in the enterprise anyway.

CB

If we put x=1, a=2 , b=5 ,$ a|x|+bx \geq 0$ becomes: $2+5\geq 0$ ,but $a\leq |b|
$ because $2\leq |5|=5$

So there are x,a,b such that :

$a|x|+bx\geq 0$ and $a\leq |b|$.

Meaning that the negation of the theorem we are trying to prove is true.

Hence the theorem itself is not true and the proof is definitely not correct
 
  • #15
First of all, I'd like to point out that this thread is full of over-quoting. For example, the quote in the previous post is completely unrelated to the post itself.

solakis said:
So there are x,a,b such that :

$a|x|+bx\geq 0$ and $a\leq |b|$.

Meaning that the negation of the theorem we are trying to prove is true.
Let's see. Below I denote "for all" by ∀. The theorem is

\[
\forall a,b,\,[(\forall x,\,a|x|+bx\ge0)\to a\ge|b|]
\]

A counterexample would be some $a$ and $b$ such that

\[
(\forall x,\,a|x|+bx\ge0)\to a\ge|b|\tag{*}
\]

is false. Since (*) is an implication, (*) is false iff $\forall x,\,a|x|+bx\ge0$ is true and $a\ge|b|$ is false, i.e., $a<|b|$ is true. However, for $a=2$ and $b=5$ you have not shown that $\forall x,\,a|x|+bx\ge0$ is true; you only gave one $x$ such that $a|x|+bx\ge0$ is true.
 
  • #16
Evgeny.Makarov said:
First of all, I'd like to point out that this thread is full of over-quoting. For example, the quote in the previous post is completely unrelated to the post itself.

Let's see. Below I denote "for all" by ∀. The theorem is

\[
\forall a,b,\,[(\forall x,\,a|x|+bx\ge0)\to a\ge|b|]
\]

A counterexample would be some $a$ and $b$ such that

\[
(\forall x,\,a|x|+bx\ge0)\to a\ge|b|\tag{*}
\]

is false. Since (*) is an implication, (*) is false iff $\forall x,\,a|x|+bx\ge0$ is true and $a\ge|b|$ is false, i.e., $a<|b|$ is true. However, for $a=2$ and $b=5$ you have not shown that $\forall x,\,a|x|+bx\ge0$ is true; you only gave one $x$ such that $a|x|+bx\ge0$ is true.
First of all we must observe a very crucial point.

To oppose my argument you had to escape in writing a complete formalization of the theorem.(is formalization one of the factors playing an important role in convincing somedoby for the correctness of a mathematical proof??)But unfortunately your argument following the complete formalization of the problem was not formal.

Now, does the forum and you want me and allow me to oppose your informal argument or must i stop here and accept as correct your argument ,because it has been written enough for the problem??
 
  • #17
solakis said:
To oppose my argument you had to escape in writing a complete formalization of the theorem.
Which argument: that the theorem is false? My explanation why your counterexample does not work is not a formalized proof. I did not build a formal derivation, either manually or using the computer. I just showed that you have not provided even an informal version of a proof of the negation of the theorem.

I made a formal derivation of the theorem itself, but then I was not opposing any argument. I was answering yes to your question whether your proof was correct.

solakis said:
(is formalization one of the factors playing an important role in convincing somedoby for the correctness of a mathematical proof??)
Usually not. It may provide additional assurance, but this is relevant only for very large proofs (several hundred pages). For usual textbook proofs, a trained mathematician is able to see if they are correct or not.

solakis said:
But unfortunately your argument following the complete formalization of the problem was not formal.
My argument that your counterexample does not work? One formalizes a proof, not an argument that something is not a proof. You offered an informal proof of the negation of the theorem; I showed informally that this proof is incorrect.

solakis said:
Now, does the forum and you want me and allow me to oppose your informal argument or must i stop here and accept as correct your argument ,because it has been written enough for the problem??
Well, if you continue arguing that your counterexample works and if you are eventually proved wrong, then you would create for yourself a reputation of a troll. And it is unlikely that the theorem is false since, as you said, you took it from a textbook and this tread was examined by several respected forum members. However, you need to fully understand for yourself what's going on.

The tricky part about this theorem is that it says

\[(\forall x,\,a|x|+bx\ge0)\to a\ge|b|\tag{1}\]

and not

\[\forall x,\,(a|x|+bx\ge0\to a\ge|b|)\tag{2}\]

If it were (2), than your counterexample would work, which means that (2) is false. As it is, the scope of universal quantifier in (1) is the assumption and not the whole formula. This means that (1) has a rather strong assumption: you have to show \(a|x|+bx\ge0\) for all x, and not just for one particular x, before you are allowed to conclude \(a\ge|b|\).

One reason I think (1) is trickier than (2) has to do with the similarity between $\forall$ and $\to$: both require an input (an instance of the quantified variable for $\forall$ and a proof of the assumption for $\to$). That is, expressions of the form $\forall x, A(x)$ and $A\to B$ behave like functions. Now, (1) is itself an implication, so it is a function that accepts a function as input. Often when one encounters such set up for the first time, the head begins to spin. In contrast, (2) is a simple function that accepts x and a proof of an inequality.
 

FAQ: Prove a|x|+bx ≥ 0 $\Rightarrow$ a ≥ |b|

How do you prove that a|x|+bx ≥ 0 implies a ≥ |b|?

To prove this statement, we can use the fact that the absolute value of a number is always greater than or equal to zero. This means that |x| ≥ 0 and |b| ≥ 0. From the given inequality, we can rewrite it as a|x| ≥ -bx. Since both sides are multiplied by a positive number, the inequality remains true. Therefore, we can conclude that a ≥ |b|.

Can you provide an example to illustrate this statement?

Sure, let's take the values a = 3 and b = -2. Substituting these values in the given inequality, we get 3|x|+(-2)x ≥ 0. Simplifying, we get 3|x| - 2x ≥ 0. Since the absolute value is always positive, 3|x| ≥ 2x. Dividing both sides by x (which is positive since it's absolute value), we get 3 ≥ 2. Therefore, our statement holds true.

Is there a specific method or formula that can be used to prove this statement?

Yes, we can use the method of proof by contradiction. We assume that a < |b| and then show that it leads to a contradiction, which proves that our assumption was incorrect and the statement is true. This method can be used for many mathematical proofs.

Can this statement be generalized to include any real numbers a and b?

Yes, this statement holds true for any real numbers a and b. This is because the absolute value of any real number is always positive and greater than or equal to zero. This allows us to rewrite the inequality as a|x| ≥ -bx, which holds true for all real numbers.

How can this statement be applied in real-life situations?

This statement has many real-life applications, especially in fields such as engineering, physics, and economics. For example, in engineering, this statement can help determine the stability of a structure by analyzing the forces acting on it. In economics, it can be used to determine the minimum production level needed to cover fixed and variable costs. Overall, this statement is a fundamental concept in mathematics and has numerous practical applications.

Back
Top