Proof Analysis: Definition & Process

[solakis1]

Browsing other forums i came across the term, proof analysis.

Most of the time the term refereed to proofs in analysis.

Other times for explaining a proof e.t.c e.t.cBut i was wondering what should be the correct definition for, proof analysis

 

[Evgeny.Makarov]

Usually in English "noun1 noun2" means "noun2 of noun1." So, "proof analysis" is analysis of proofs. Similarly, proofs in analysis could be referred to by "analysis proofs."

Proofs can be analyzed from many standpoints. For example, one may study the minimum lengths of proofs of statements of a certain class in a certain formal system. Proofs are distinguished by what axioms they use. For instance, proofs that don't use double-negation elimination or the law of excluded middle (and some other principles) are called constructive, and they have special property: they contain an algorithm for building objects whose existence they prove. Proofs are also distinguished by whether they use the axiom of choice, which has some counterintuitive consequences. There is a whole are of logic called reverse mathematics, which studies axioms necessary to prove certain well-known theorems, such as the Bolzano–Weierstrass theorem. There is also an area called proof mining. "In proof theory, a branch of mathematical logic, proof mining (or unwinding) is a research program that analyzes formalized proofs, especially in analysis, to obtain explicit bounds or rates of convergence from proofs" (emphasis mine) (Wikipedia).

 

[solakis1]

for example if we were to proof analyze the following theorem in analysis:

if:

1) $f:A\subset R \Longrightarrow R$

2) a is an accumulation point of A

3)$ f(x)\geq 0$ for all xεA

4) $Lim_{x\to a} f(x) = l$

Then:

$l\geq 0$.

What should we do??

 

[Evgeny.Makarov]

First, you need a proof to analyze. Second, you need to say from which standpoint you want it analyzed, i.e., what you want to determine.

 

[solakis1]

First, you need a proof to analyze. Second, you need to say from which standpoint you want it analyzed, i.e., what you want to determine.

O.K let us say that on the following proof :

Suppose l<0 ,then put ε =-l.

Then there exists a δ>0 such that :

|f(x)-l|<-l whenever 0<|x-a|<δ.

But $ |f(x)-l|<-l \Longleftrightarrow l<f(x)-l<-l \Longrightarrow f(x)<0 \Longrightarrow 0\leq f(x)<0 \Longrightarrow 0<0$ a contradiction

Hence :$l\geq 0$

We want to:

Proofs can be analyzed from many standpoints. For example, one may study the minimum lengths of proofs of statements of a certain class in a certain formal system.

 

[jakncoke1]

proof analysis is not an analysis proof. Proof analysis is studying a proof and understanding the teChniques used in the proof, asserting what impliCit assumpitions were made, determining if the proof is even valid, and perhaps examining Corolarries that might follow if the proof was deemed Corret.

 

[solakis1]

proof analysis is not an analysis proof. Proof analysis is studying a proof and understanding the teChniques used in the proof, asserting what impliCit assumpitions were made, determining if the proof is even valid, and perhaps examining Corolarries that might follow if the proof was deemed Corret.

Why can't you have a proof analysis in an analysis proof??

Can you give an example showing the technics taking place in the proof and what assumptions were made??

 

[jakncoke1]

Why can't you have a proof analysis in an analysis proof??

Can you give an example showing the technics taking place in the proof and what assumptions were made??

you can have a proof analysis in an analysis proof but proof analysis can be extended to any proof, analysis or otherwise

For example. If someone posted a proof like the following

Take $a \in \mathbb{Z}_{4}$ and assume 2*a = 2*2. Then by cancellation property this implies a = 2.
QED

Now if i were to do an analysis of this, i would note that this person was assuming the left cancellation law which states if ab=ac then b = c. I would also note that this cancellation law fails in $\mathbb{Z}_{4}$ because it is not an integral domain, i.e, there are zero divisors in $\mathbb{Z}_{4}$ (2*2 $\in \mathbb{Z}_{4} = 0$

This is a very simple example of analysis of a proof (which happens to be wrong but you can also do one of a proof which is correct)

 

[solakis1]

you can have a proof analysis in an analysis proof but proof analysis can be extended to any proof, analysis or otherwise

For example. If someone posted a proof like the following

Take $a \in \mathbb{Z}_{4}$ and assume 2*a = 2*2. Then by cancellation property this implies a = 2.
QED

Now if i were to do an analysis of this, i would note that this person was assuming the left cancellation law which states if ab=ac then b = c. I would also note that this cancellation law fails in $\mathbb{Z}_{4}$ because it is not an integral domain, i.e, there are zero divisors in $\mathbb{Z}_{4}$ (2*2 $\in \mathbb{Z}_{4} = 0$

This is a very simple example of analysis of a proof (which happens to be wrong but you can also do one of a proof which is correct)

Good . i can follow
Let us extent your method to another very simple well known theorem in real Nos.

In proving : 0x =0 for all x the following proof is suggested:

0x = 0x +0 = 0x +(x+(-x)) = (0x+x)+(-x)= (0+1)x +(-x) = x+(-x) = 0

What are the assumptions and the technic followed here??

 

[jakncoke1]

Good . i can follow
Let us extent your method to another very simple well known theorem in real Nos.

In proving : 0x =0 for all x the following proof is suggested:

0x = 0x +0 = 0x +(x+(-x)) = (0x+x)+(-x)= (0+1)x +(-x) = x+(-x) = 0

What are the assumptions and the technic followed here??

Here are some of the assumptions.

If you had operation was +, * defined on the set of real Numbers. Then you are implicity assuming these following:
Assosiativity: where you say 0x + (x+(-x)) = (0x+x)+(-x)
Right Distributivity: where you say (0x + x) = (0+1)x
That any element x has an additive inverse denoted -x
these are just some of the assumptions

The method followed in your proof was straight forward, you start with premise and use the axioms to derive the result.

Usually the techniques are not mentioned unless it is novel. I've seen some proof which use techniques which you think to yourself (Where the hell did that come out of and where is he going with this?) but they end up proving their assertion in the end and the technique is usually written about in the analysis.

Cantor's diagnolization argument is a good example of a novel technique

We know that all of these assertions hold for ($\mathbb{R}$, +, *), but in your proof these are implicity assumed.

 

[solakis1]

Here are some of the assumptions.

If you had operation was +, * defined on the set of real Numbers. Then you are implicity assuming these following:
Assosiativity: where you say 0x + (x+(-x)) = (0x+x)+(-x)
Right Distributivity: where you say (0x + x) = (0+1)x
That any element x has an additive inverse denoted -x
these are just some of the assumptions

The method followed in your proof was straight forward, you start with premise and use the axioms to derive the result.

Usually the techniques are not mentioned unless it is novel. I've seen some proof which use techniques which you think to yourself (Where the hell did that come out of and where is he going with this?) but they end up proving their assertion in the end and the technique is usually written about in the analysis.

Cantor's diagnolization argument is a good example of a novel technique

We know that all of these assertions hold for ($\mathbb{R}$, +, *), but in your proof these are implicity assumed.

Thank you i agree.

What then do you suppose are the assumptions in the proof of post No 5??

 

[jakncoke1]

you explicity assumed these

1) $f:A\subset R \Longrightarrow R$

2) a is an accumulation point of A

3)$ f(x)\geq 0$ for all xεA

4) $Lim_{x\to a} f(x) = l$

Then you also assumed $l < 0$ to derive a contradiction

You also assumed implicitly that the $\mathbb{R}$ under addition is a ordered group. Which means first of all, any 2 elements, $a,b \in (\mathbb{R},+)$ equipped with partial order $\leq$ are comprable, so either $a \leq b$ or $b \leq a$ and for $a,b \in G$ with $a \leq b$ then for $c \in G$, $a + c \leq b + c$ and $c + a \leq c + b$.

 

[Evgeny.Makarov]

O.K let us say that on the following proof :

Suppose l<0 ,then put ε =-l.

Then there exists a δ>0 such that :

|f(x)-l|<-l whenever 0<|x-a|<δ.

But $ |f(x)-l|<-l \Longleftrightarrow l<f(x)-l<-l \Longrightarrow f(x)<0 \Longrightarrow 0\leq f(x)<0 \Longrightarrow 0<0$ a contradiction

Hence :$l\geq 0$

I don't see how $f(x)<0$ implies $0\leq f(x)<0$. Neither is this conclusion implied by $l<f(x)-l<-l$. If you add $l$ to all sides, you get $2l<f(x)<0$. So, the contradiction comes not from the fact that 0 < 0, but from $f(x)<0$ because the assumptions says that $f(x)\ge0$ for all $x\in A$. Concerning the latter claim, your proof does not say what $x$ is and why $x\in A$. Since $l$ is an accumulation point of $A$, for every neighborhood of $l$, including the one with the given $\delta$, there exists some $x\in A$ in this neighborhood, and this is the $x$ we use in the rest of the proof.

We want to:

Proofs can be analyzed from many standpoints. For example, one may study the minimum lengths of proofs of statements of a certain class in a certain formal system.

The study of proof complexity usually concerns propositional proofs.

 

[solakis1]

I don't see how $f(x)<0$ implies $0\leq f(x)<0$. Neither is this conclusion implied by $l<f(x)-l<-l$. If you add $l$ to all sides, you get $2l<f(x)<0$. So, the contradiction comes not from the fact that 0 < 0, but from $f(x)<0$ because the assumptions says that $f(x)\ge0$ for all $x\in A$. Concerning the latter claim, your proof does not say what $x$ is and why $x\in A$. Since $l$ is an accumulation point of $A$, for every neighborhood of $l$, including the one with the given $\delta$, there exists some $x\in A$ in this neighborhood, and this is the $x$ we use in the rest of the proof.

The study of proof complexity usually concerns propositional proofs.

To be pricize the exact expression that i did not use in my derivation is :

|f(x)-l|<-l whenever xεΑ and 0|x-a|<δ ,instead of :

|f(x)-l|<-l whenever 0|x-a|<δ that i used in my derivation.
Then this is the same x for which :

$f(x)\geq 0 $ and f(x)<0, hence $0\leq f(x)<0\Longrightarrow 0<0$ a contradictionAnd now can we do proof mining to the above proof according to:

"In proof theory, a branch of mathematical logic, proof mining (or unwinding) is a research program that analyzes formalized proofs, especially in analysis, to obtain explicit bounds or rates of convergence from proofs"

 

[Evgeny.Makarov]

To be pricize the exact expression that i did not use in my derivation is :

|f(x)-l|<-l whenever xεΑ and 0|x-a|<δ ,instead of :

|f(x)-l|<-l whenever 0|x-a|<δ that i used in my derivation.
Then this is the same x for which :

$f(x)\geq 0 $ and f(x)<0, hence $0\leq f(x)<0\Longrightarrow 0<0$ a contradiction

Ah, I see. Sorry, I did not realize that you used the assumption that $f(x)\ge0$ in the string of implications. For this reason, one should not hesitate to include plain English in a proof. Instead of $l<f(x)-l<-l \Longrightarrow f(x)<0 \Longrightarrow 0\leq f(x)<0$, which gives an impression that $f(x)<0$ alone implies $0\leq f(x)<0$, I would write, "$l<f(x)-l<-l \Longrightarrow f(x)<0$, which, together with the assumption that $f(x)\ge0$ for all $x\in A$, implies $0\leq f(x)<0$."

Still, in order to instantiate the definition of limit with some $x\in A$ from the $\delta$-neighborhood of $l$, you need to prove that such $x$ exists. This requires invoking the fact that $l$ is an accumulation point. This has been glossed over in the proof.

 

[solakis1]

you explicity assumed these

1) $f:A\subset R \Longrightarrow R$

2) a is an accumulation point of A

3)$ f(x)\geq 0$ for all xεA

4) $Lim_{x\to a} f(x) = l$

Then you also assumed $l < 0$ to derive a contradiction

You also assumed implicitly that the $\mathbb{R}$ under addition is a ordered group. Which means first of all, any 2 elements, $a,b \in (\mathbb{R},+)$ equipped with partial order $\leq$ are comprable, so either $a \leq b$ or $b \leq a$ and for $a,b \in G$ with $a \leq b$ then for $c \in G$, $a + c \leq b + c$ and $c + a \leq c + b$.

Now i am a little stuck .

Where exactly in my proof do we use:

"so either $a \leq b$ or $b \leq a$ and for $a,b \in G$ with $a \leq b$ then for $c \in G$, $a + c \leq b + c$ and $c + a \leq c + b$"

These two assumptions??

 

[jakncoke1]

Now i am a little stuck .

Where exactly in my proof do we use:

"so either $a \leq b$ or $b \leq a$ and for $a,b \in G$ with $a \leq b$ then for $c \in G$, $a + c \leq b + c$ and $c + a \leq c + b$"

These two assumptions??

the $\leq$ is a partial ordering(it is not the less than or equal). The less than or equal is one partial ordering that is possible in this case(it is confusing because the symbol $\leq$ is used to describe the less than equal partial order and any type of general partial order) , the less than is another partial ordering that is possible on the set of real numbers with addition operation, so in this case we can substitue $\leq$ with $<$ for concreteness.

You used this property when you did $l < f(x) - l < -l$, you added l to $f(x)-l+l < -l + l$ to get $f(x) < 0$. if a = $f(x)-l$ and b=$-l$
arent you assuming $a < b$(total order), and $a + l < b + l $

 

[solakis1]

Still, in order to instantiate the definition of limit with some $x\in A$ from the $\delta$-neighborhood of $l$, you need to prove that such $x$ exists. This requires invoking the fact that $l$ is an accumulation point. This has been glossed over in the proof.

Now we come into a point that :

You think that we must specialize an x along the proof .

And i do not this as necessary because in many proofs in analysis the presence of an accumulation point is not used in the proof at all.

What shall we do now??

 

[Evgeny.Makarov]

You think that we must specialize an x along the proof .

And i do not this as necessary because in many proofs in analysis the presence of an accumulation point is not used in the proof at all.

In a correct proof, every used variable should be properly introduced. Just like in a regular conversation, if your friend told you that Pennington is an ambidexter, you may have no idea what he/she is talking about because none of the people you know is called Pennington. Some of the ways to introduce x are: "Let x = ...", "Fix an arbitrary x in A" (provided it has been shown that A is nonempty), "Consider x whose existence is claimed by (1)" (provided formula (1) is proved earlier).

Suppose l<0 ,then put ε =-l.

Then there exists a δ>0 such that :

|f(x)-l|<-l whenever 0<|x-a|<δ.

But $|f(x)−l|<−l⟺\iff{}$...

Here the use of x in the second last line is OK because it means |f(x) - l| < -l for all x such that 0 < |x - a| < δ. "For all" makes x range over the whole neighborhood. However, in the last line you are talking about some concrete x, and it is not clear what it is. This is not allowed in a well-formed proof. If you say that x is universally quantified over the whole last line, that's fine, but since you are using the assumption $f(x)\ge 0$, which is true only for $x\in A$, x must be quantified over those elements of the neighborhood that belong to $A$.And if this set is empty, then you have not proved anything because a statement that starts by universally quantifying over the empty set is vacuously true. I don't believe you think that x has to be quantified over in the last line, so you have to say what this x is.

An argument from another side is that this theorem is false in general if $l$ is not an accumulation point of A. Can you find a counterexample?

 

[solakis1]

the $\leq$ is a partial ordering(it is not the less than or equal). The less than or equal is one partial ordering that is possible in this case(it is confusing because the symbol $\leq$ is used to describe the less than equal partial order and any type of general partial order) , the less than is another partial ordering that is possible on the set of real numbers with addition operation, so in this case we can substitue $\leq$ with $<$ for concreteness.

You used this property when you did $l < f(x) - l < -l$, you added l to $f(x)-l+l < -l + l$ to get $f(x) < 0$. if a = $f(x)-l$ and b=$-l$
arent you assuming $a < b$(total order), and $a + l < b + l $

Yes , i agree now .

But the assumption : "a<b <=> a+c<b+c ,for alla,b,c" ,is the only assumption implicitly used in my proof?

 

[solakis1]

In a correct proof, every used variable should be properly introduced. Just like in a regular conversation, if your friend told you that Pennington is an ambidexter, you may have no idea what he/she is talking about because none of the people you know is called Pennington. Some of the ways to introduce x are: "Let x = ...", "Fix an arbitrary x in A" (provided it has been shown that A is nonempty), "Consider x whose existence is claimed by (1)" (provided formula (1) is proved earlier).

Here the use of x in the second last line is OK because it means |f(x) - l| < -l for all x such that 0 < |x - a| < δ. "For all" makes x range over the whole neighborhood. However, in the last line you are talking about some concrete x, and it is not clear what it is. This is not allowed in a well-formed proof. If you say that x is universally quantified over the whole last line, that's fine, but since you are using the assumption $f(x)\ge 0$, which is true only for $x\in A$, x must be quantified over those elements of the neighborhood that belong to $A$.And if this set is empty, then you have not proved anything because a statement that starts by universally quantifying over the empty set is vacuously true. I don't believe you think that x has to be quantified over in the last line, so you have to say what this x is.

An argument from another side is that this theorem is false in general if $l$ is not an accumulation point of A. Can you find a counterexample?

Look at the following proof concerning the uniqueness of the limit: when a Limit of a function f(z) exists at a point a,it is unique.To do this ,we suppose thatlim f(z) =l and lim f(z)=m as z----> a (z goes to a).Then,for any positive number ε,there are positive numbers r,δ such that

|f(z)-l |< ε whenever 0< |z-a |<r

and

|f(z)-m |<ε whenever 0< |z-a |<δSo if 0< |z-a |<θ ,where θ denotes the smaller of the two Nos r and δ,we find that

|l-m |= |(f(z)-m)-(f(z)-l) |=< |f(z)-l | + |f(z)-m | < ε +ε=2ε But |l-m | is a nonnegative constant, and ε can be chosen arbitrarily small.
Hence

l-m =0 , or l=m."

Here we use z instead of x and as you can see the z ranges over the domain of f.

WE have no specialization of z .

And we do not use the property of a which is an accumulation point.

The structure of the proof is similar to my proof .

Do you think that this proof is not 100% correct??

 

[jakncoke1]

Look at the following proof concerning the uniqueness of the limit: when a Limit of a function f(z) exists at a point a,it is unique.To do this ,we suppose thatlim f(z) =l and lim f(z)=m as z----> a (z goes to a).Then,for any positive number ε,there are positive numbers r,δ such that

|f(z)-l |< ε whenever 0< |z-a |<r

and

|f(z)-m |<ε whenever 0< |z-a |<δSo if 0< |z-a |<θ ,where θ denotes the smaller of the two Nos r and δ,we find that

|l-m |= |(f(z)-m)-(f(z)-l) |=< |f(z)-l | + |f(z)-m | < ε +ε=2ε But |l-m | is a nonnegative constant, and ε can be chosen arbitrarily small.
Hence

l-m =0 , or l=m."

Here we use z instead of x and as you can see the z ranges over the domain of f.

WE have no specialization of z .

And we do not use the property of a which is an accumulation point.

The structure of the proof is similar to my proof .

Do you think that this proof is not 100% correct??

It looks correct but I'm not sure why you have to say "here we use z instead of x", i To do this ,we suppose that"dont see what difference that would make. and again, I'm only being pedantic because you seem to want that but

"when a Limit of a function f(z) exists at a point a,it is unique." This statement only holds, in general, if a space is Hausdorff.

 

[solakis1]

It looks correct but I'm not sure why you have to say "here we use z instead of x", i To do this ,we suppose that"dont see what difference that would make. and again, I'm only being pedantic because you seem to want that but

"when a Limit of a function f(z) exists at a point a,it is unique." This statement only holds, in general, if a space is Hausdorff.

If you read the previous posts of EMakarov you will see that she insisted that i should specialize the x variable that i used in my proof .

So as an of example i posted the above proof where we do not have specialization of z (an x in my proof).

Although we have the presence of an accumulation point (a) like we have in my proof.