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

[solakis1]

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

 

[Evgeny.Makarov]

Is that proof correct??

Yes.

 

[solakis1]

Yes.

Can you have : x=1 and x=-1 ??

 

[Ackbach]

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.

 

[solakis1]

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$

 

[Ackbach]

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.

 

[solakis1]

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

 

[CaptainBlack]

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

 

[Evgeny.Makarov]

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:

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.

 

[Evgeny.Makarov]

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.

 

[solakis1]

I formalized the proof. It uses several lemmas:

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

 

[Evgeny.Makarov]

Meaning that the proof is correct??

Yes.

...

 

[CaptainBlack]

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

 

[solakis1]

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

 

[Evgeny.Makarov]

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.

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.

 

[solakis1]

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

 

[Evgeny.Makarov]

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.

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

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.

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.