7 ms·

If I were allowed a small philosophical leeway, I'd argue that two correct proofs are always the same. For sure they may contain different words or make use of

by pkoird 2y ago

If I were allowed a small philosophical leeway, I'd argue that two correct proofs are always the same. For sure they may contain different words or make use of different "abstractions", but it just seems to me that these abstractions should be equivalent if one were willing to unravel it all to a certain degree. Essentially, all proof is, is a statement that says "this is true" and no matter which language you use to say it, you are saying the same thing.

deleted 2y ago
[deleted]
ColinWright 2y ago
This is like saying that if I walk out of my house, turn right, and walk 10 minutes to the local food store, it's the same as coming out of the house, turning left, and walking 15 minutes around the block. The destination is the same, so surely these are "the same". I'd argue that this is not the case.
- lupire 2y ago
  There's a simple mechanical transformation from one path to the other. As a proof that "the store is reachable, they are essentially the same if it is already known that you live on a "block" with the store" . If it is not known that you live on a block, then the second proof together with the first gives a much deeper result, proving that you do live on a block. That makes a second proof valuable, but in the monograph of history, it is most parsimonious to make the block proof and the note how it implies to trivially distinct ways of reaching the store.
  - ColinWright 2y ago
    So you are saying that the two proofs are different, but there is a third proof that gives each of the first two as corollaries. So ... the first two proofs are different, then.
    - lupire 2y ago
      That's one opinion. The OP and I have a different opinion.
  - Y_Y 2y ago
    Neglect considerations of homotopy at your peril!
    - gus_massa 2y ago
      Yep. If you can go from A to C by B or B' and all the place is a nice grass field they are probably equivalent. But if between B anb B' there is an active vocano, most people would call the paths different.
- pkoird 2y ago
  Not quite. If we consider that we are trying to prove "you can reach the local food store from your house" then starting from either side would consist of two proofs by example. And for sure these are different paths one is taking and should be different! But if you consider deeply, both of these proofs are implicitly encoding same information about the space between your house and the local store: 1) there is continuous space between your house and the store i.e. the store is reachable from your house. (as opposed to your house being in on an island and you not being able to swim) 2) you can traverse two points in a continuous space. What I wanted to opine was merely the fact that since all proofs use logic, assuming certain premise, all theorems about a certain statement being true must be reducible to a single irreducible logical chain of argument. It is true that we use different abstractions that have relevant meaning and ease in different contexts but since all of our abstractions are based upon logic in the first place, it does not seem outlandish to me to think that any logical transformation and subsequent treatment between two proof structures should inherently encode the same facts.
  - Twisol 2y ago
    The path example is extremely fertile ground for this kind of discussion! It is definitely true that both paths encode the information that one's house is connected to the local store. But is that all they encode? Homotopy theory is all about the different paths between two points, and it tells us some quite interesting things! In particular, if you have two paths from point A to point B, you can ask: can you smoothly animate an image of the first path into an image of the second, such that every still frame in-between is also a legitimate path? (If you can't, that tells you that there's some form of hole in between them!) In the house/store example, a path is also a witness to the fact that, if you perform a road closure anywhere not on the path, then connectivity is preserved. Simply stating that the two points are connected doesn't tell you whether it's safe to close a road! Moreover, taking the two paths together tells you that performing a single road closure that only affects one of the paths will still leave a route you can take. In both examples, if the paths were logically interchangeable, you wouldn't be able to get more information out of the both of them than you could from just one. But because they aren't equivalent -- because each contains some information that the other does not -- we can deduce more from both together than from either individually.
shaunxcode 2y ago
yes : if two discrete semiotic symbolic networks point to the same signified value they are the same in the way two different poems with the same meaning are the same. which is to say they are unique but have the same meaning.
drdeca 2y ago
A proof is not a statement that something is true, but a demonstration that it is true. Are you familiar with the proofs-as-programs idea? The uh, something isomorphism? Idr the name. Not all programs that implement a function are the same. When you boil things down to the fundamental steps of the logic you are working on, you needn’t get the same thing. For one thing, it may be that axioms A and B suffice to prove Z, and that axioms B and C suffice to prove Z, but that B alone doesn’t, and that A and B doesn’t prove C and that B and C doesn’t prove A. So, the proofs using A and the proofs using C are certainly different.
- js8 2y ago
  I think "propositions-as-types" is exactly why we should consider proofs to be the same if they prove the same type. As others have already said, if you want to distinguish between different proofs, it's better to encode those distinctions formally into types (and thus potentially into another mathematical theory).
  - drdeca 2y ago
    There are multiple values of type integer? I don’t see why we should truncate the types representing propositions so that they have at most one element each.
    - js8 2y ago
      We shouldn't, that's the point! At least not in mathematics, programming is a different story. It's perfectly fine to have type of all integers alongside type of all squares and types that only contain number 1 or number 1729. Relations of these types will then reflect the relations of their respective proofs. There is no need to consider "proof equivalence" or other kind of proof properties. That's already accomplished by studying types themselves. The choice of types already reflects what we want to study.
      - drdeca 2y ago
        I would think that asking if two proofs are equivalent would be analogous to “do these two expressions of type integer evaluate to the same value?” ?
Twisol 2y ago
I disagree with this on two points. First, oftentimes the interest in proving long-standing, difficult mathematical problems is because we hope a proof will demonstrate new tools for tackling similar problems. In that sense, the exact content of a proof is quite important. Not to mention, there is value in having multiple proofs that each demonstrate quite different toolkits. Mere truth is not often the most important thing -- after all, mathematicians can (and do!) take certain propositions as premises of downstream work. If we discover a proof for one of those premises, that just means we can drop the premise from downstream work. Not having a proof doesn't block us from making use of the proposition anyway. Second, sometimes the content of the proof is relevant formally. A sibling comment gave an example in terms of paths between two points; it is often the case that you care not only that the points are merely connected, but you also have a preference for which path is taken. Or, you can do an analysis of the paths themselves, and determine their length or average furthest distance from the nearest McDonalds. A path is "just" a proof of connectivity, but the individual paths can be quite distinct when studied themselves. Less abstractly, a constructive proof will yield an algorithm that can be performed, and we know quite well that the variety of sorting algorithms (that "merely" prove that "all lists are sortable") actually vary in quite important ways, including asymptotics and stability.
- lupire 2y ago
  Asymptotics and stability are different theorems. An algorithm is not a proof. It is a technique for proof. Two algorithms can be different, while not being meaningfully different profs that a list is sortable. To the extent that they are different, they proof different theorems, such as "list can be sorted in O(f) time" for an f of interest.
  - Twisol 2y ago
    > An algorithm is not a proof. That is an opinion that many do not share. FWIW, I framed my response as an opinion; you gave yours as a blanket statement. It is not wrong to treat algorithms as valid proofs. In a dependent type theory, propositions are represented as types; the proposition that "all lists can be sorted" could be represented represented as the type "forall (t : Type) -> (le : Ordered t) -> forall (xs : List t) -> exists (ys : List t). (Increasing le ys, PermutationOf xs ys)". A proof of this proposition is exactly a program (algorithm) with that type; the sorted list is the `ys` component of the returned existential product. Yet the inhabitants of this type are not graded by asymptotics or stability; any sorting algorithm will do. In a setting where inhabitants of the above type are distinguishable, you could then write proofs of asymptotics or stability against individual algorithms. That is, the proofs of the sorting proposition are themselves the subjects of subsequent propositions and proofs thereof.
lupire 2y ago
A Proof is not a statement. A theorem is a statement. Proofs are usually not completely formal or even formalizable. Math is not completely well founded. "Unravelling it all the way" might be an open research project, or a new conjecture directly inspired by the second, apparently different proof. Showing these two profs to be equivalent might depend on a major new idea that happens after the two proofs are createdm This is hinted at in the OP discussion of Terry Tao.
- bjornsing 2y ago
  > Proofs are usually not completely formal or even formalizable. Math is not completely well founded. This is often stated, but is it really true? I haven’t seen a persuasive argument that not all math could (in principle) be formalized.
justinpombrio 2y ago
Some proofs that aren't "essentially the same": 1. Prove that the interior angles of a triangle sum to 180 degrees. First proof: draw a line parallel to one of the triangle's sides passing through its opposite vertex. There are three angles on one side of this line, and they obviously add to 180 degrees because it's a line. One of the three angles is directly one of the triangle's interior angles; the other two can be shown to be equal to the triangle's other two interior angles. (Try drawing it out.) Second proof: start at one side of the triangle and walk around it. By the time you return to where you started, you must have turned 360 degrees. Thus the sum of the exterior angles is 360 degrees. Each interior angle is 180 minus the corresponding exterior angle, and there are three of them, so calling the interior angles A, B, C and the exterior angles A', B', C' we have A'+B'+C' = 360 implies (180-A) + (180-B) + (180-C) = 360 implies 540 - A - B - C = 360 implies 180 = A + B + C. 2. Prove that the sum of the first N numbers is N(N+1)/2. First proof: sum the first and last number to get 1 + N, then the second and second-to-last to get 2 + (N-1) = 1 + N, repeating until you get to the middle. There are N/2 such pairs, giving a total of (1 + N)N/2. (This assumed that there were an even number of terms; consider the odd case too.) Second proof: proceed by induction. For the base case, it's true for N=1 because 1*2/2 = 1. For the inductive case, suppose it's true for N-1. Then 1 + 2 + ... + N-1 + N = (1 + 2 + ... + N-1) + N = N(N-1)/2 + N = N(N-1)/2 + 2N/2 = N(N+1)/2.
- pkoird 2y ago
  I'm responding to your second example simply because it's easy to argue about. I'd say that both proofs that you have presented are equivalent ways of saying that "since when you sum all the numbers from 1 to N you obtain a number that's N(N+1)/2, therefore, it is true that the sum of numbers from 1 to N is N(N+1)/2". Now, this argument may appear trite but do consider that both of your proofs essentially do the same thing with the first one summing the numbers from extremities and the second one summing 1...N-1 first and then the last. I'd argue that if addition were not commutative, you may have obtained different results.
  - justinpombrio 2y ago
    If two programs are equivalent, you can typically show that they're equivalent with a sequence of small refactorings. Replace `x + x` with `2 * x`. Inline that function call. Etc. Can you do that with these two proofs? What's a proof that's halfway in between the two? If you can get from one proof to the other with small "refactorings", then I agree that they're fundamentally the same. If you can't---if there's an insurmountable gap that you need to leap across to transform one into the other---then I'd call them fundamentally different. If you insist that two proofs are "essentially the same thing" despite having this uncrossable gap between them, then I suspect you're defining "essentially the same" to mean "proves the same thing", which is a stupid definition because it makes all proofs the same by fiat, and avoids the interesting question.
Someone 2y ago
Theorem: there are 500,000 odd integers between zero and a million. Proof #1: there ar no odd integers between zero and 1 (inclusive), 1 is odd so there is 1 odd integer between zero and 2, 2 is even so there is 1 odd integer between zero and 3, 3 is odd so there are 2 odd integers between zero and 4, …, 999,998 is even so there are 499,999 odd integers between zero and 999,999, 999,999 is odd so there are 500,000 odd integers between zero and 1,000,000. QED. Proof #2: this is a specific case of “there are n odd integers between zero and 2n (exclusive)”. (proof of the more general theorem). Picking n to be 500,000, the theorem follows. I think most people would call those two proofs different.
winwang 2y ago
Two programs which are semantically equivalent are not simply the same. See: bubblesort vs mergesort. (Yes I'm relying on curry-howard isomorphism here).
- andrewla 2y ago
  I don't know why this hasn't been voted to the top. Curry-Howard isomorphism is a hell of a bludgeon to apply here but it makes for a very straightforward and obvious refutation of the parent post.
seanhunter 2y ago
I don't think this is true because a proof does more than state a conclusion. It establishes a true path from some premises to that conclusion. Sometimes that path continues. For example if you had a general constructive proof that there were infinitely many prime numbers it should be a simple matter to alter it a bit and prove the twin prime conjecture wouldn't it? In general a constructive proof and a non-constructive proof of some fact (say proof by contradiction) are fundamentally different in terms of where you can go with the proof.
naniwaduni 2y ago
> I'd argue that two correct proofs are always the same All correct inferences proceeding from the same axioms are the same.
tightbookkeeper 2y ago
No. Because the whole point of proof from a human perspective is to express understanding of the question, not merely answer it.
mjcohen 2y ago
How abut the following proofs that sqrt{2} is irrational. 1. If 2=a^2/b^2 with a and b relatively prime then a^2=2b^2 so a is even, and, letting a=2c, b is also even a contradiction. 2. Use the lemma that a positive real r is rational if and only if there is a positive integer b such that br is an integer. (Proof left to the reader.) if sqrt{2} is ration then there is an integer b such that bsqrt{2}=a for some integer a. Let b be the smallest such integer. Then, if c=b(sqrt{2}-1) then c is smaller than b, c=bsqrt{2}-b is an integer, and sqrt{2}c=sqrt{2}b(sqrt{2}-1)=2b-b*sqrt{2} is an integer, a contradiction (this uses infinite descent). 3. Use the theorem that if x, y, and n are positive integers such that x^2-ny^2=1 then sqrt{n} is irrational, and apply with n=2, x=3, y=2. Proof of theorem. a. If x^2-ny^2=1, then using (x^2-ny^2)^2=(x^2+ny^2)^2-n(2xy)^2 to show that there are arbitrarily large solutions to x^2-ny^2=1. b. If n=a^2/b^2 then 1=x^2-(a^2/b^2)y^2 so b^2=b^2x^2-a^2y^2=(bx+ay)(bx-ay)>=bx+ay>bx so b>x but this contradicts the existence of arbitrarily large x. How are any of these the same as any other?

by pkoird 2y ago

deleted 2y ago

[deleted]

ColinWright 2y ago

This is like saying that if I walk out of my house, turn right, and walk 10 minutes to the local food store, it's the same as coming out of the house, turning left, and walking 15 minutes around the block. The destination is the same, so surely these are "the same". I'd argue that this is not the case.

lupire 2y ago
There's a simple mechanical transformation from one path to the other. As a proof that "the store is reachable, they are essentially the same if it is already known that you live on a "block" with the store" . If it is not known that you live on a block, then the second proof together with the first gives a much deeper result, proving that you do live on a block. That makes a second proof valuable, but in the monograph of history, it is most parsimonious to make the block proof and the note how it implies to trivially distinct ways of reaching the store.
- ColinWright 2y ago
  So you are saying that the two proofs are different, but there is a third proof that gives each of the first two as corollaries. So ... the first two proofs are different, then.
  - lupire 2y ago
    That's one opinion. The OP and I have a different opinion.
- Y_Y 2y ago
  Neglect considerations of homotopy at your peril!
  - gus_massa 2y ago
    Yep. If you can go from A to C by B or B' and all the place is a nice grass field they are probably equivalent. But if between B anb B' there is an active vocano, most people would call the paths different.
pkoird 2y ago
Not quite. If we consider that we are trying to prove "you can reach the local food store from your house" then starting from either side would consist of two proofs by example. And for sure these are different paths one is taking and should be different! But if you consider deeply, both of these proofs are implicitly encoding same information about the space between your house and the local store: 1) there is continuous space between your house and the store i.e. the store is reachable from your house. (as opposed to your house being in on an island and you not being able to swim) 2) you can traverse two points in a continuous space. What I wanted to opine was merely the fact that since all proofs use logic, assuming certain premise, all theorems about a certain statement being true must be reducible to a single irreducible logical chain of argument. It is true that we use different abstractions that have relevant meaning and ease in different contexts but since all of our abstractions are based upon logic in the first place, it does not seem outlandish to me to think that any logical transformation and subsequent treatment between two proof structures should inherently encode the same facts.
- Twisol 2y ago
  The path example is extremely fertile ground for this kind of discussion! It is definitely true that both paths encode the information that one's house is connected to the local store. But is that all they encode? Homotopy theory is all about the different paths between two points, and it tells us some quite interesting things! In particular, if you have two paths from point A to point B, you can ask: can you smoothly animate an image of the first path into an image of the second, such that every still frame in-between is also a legitimate path? (If you can't, that tells you that there's some form of hole in between them!) In the house/store example, a path is also a witness to the fact that, if you perform a road closure anywhere not on the path, then connectivity is preserved. Simply stating that the two points are connected doesn't tell you whether it's safe to close a road! Moreover, taking the two paths together tells you that performing a single road closure that only affects one of the paths will still leave a route you can take. In both examples, if the paths were logically interchangeable, you wouldn't be able to get more information out of the both of them than you could from just one. But because they aren't equivalent -- because each contains some information that the other does not -- we can deduce more from both together than from either individually.

shaunxcode 2y ago

yes : if two discrete semiotic symbolic networks point to the same signified value they are the same in the way two different poems with the same meaning are the same. which is to say they are unique but have the same meaning.

drdeca 2y ago

A proof is not a statement that something is true, but a demonstration that it is true. Are you familiar with the proofs-as-programs idea? The uh, something isomorphism? Idr the name. Not all programs that implement a function are the same. When you boil things down to the fundamental steps of the logic you are working on, you needn’t get the same thing. For one thing, it may be that axioms A and B suffice to prove Z, and that axioms B and C suffice to prove Z, but that B alone doesn’t, and that A and B doesn’t prove C and that B and C doesn’t prove A. So, the proofs using A and the proofs using C are certainly different.

js8 2y ago
I think "propositions-as-types" is exactly why we should consider proofs to be the same if they prove the same type. As others have already said, if you want to distinguish between different proofs, it's better to encode those distinctions formally into types (and thus potentially into another mathematical theory).
- drdeca 2y ago
  There are multiple values of type integer? I don’t see why we should truncate the types representing propositions so that they have at most one element each.
  - js8 2y ago
    We shouldn't, that's the point! At least not in mathematics, programming is a different story. It's perfectly fine to have type of all integers alongside type of all squares and types that only contain number 1 or number 1729. Relations of these types will then reflect the relations of their respective proofs. There is no need to consider "proof equivalence" or other kind of proof properties. That's already accomplished by studying types themselves. The choice of types already reflects what we want to study.
    - drdeca 2y ago
      I would think that asking if two proofs are equivalent would be analogous to “do these two expressions of type integer evaluate to the same value?” ?

Twisol 2y ago

I disagree with this on two points. First, oftentimes the interest in proving long-standing, difficult mathematical problems is because we hope a proof will demonstrate new tools for tackling similar problems. In that sense, the exact content of a proof is quite important. Not to mention, there is value in having multiple proofs that each demonstrate quite different toolkits. Mere truth is not often the most important thing -- after all, mathematicians can (and do!) take certain propositions as premises of downstream work. If we discover a proof for one of those premises, that just means we can drop the premise from downstream work. Not having a proof doesn't block us from making use of the proposition anyway. Second, sometimes the content of the proof is relevant formally. A sibling comment gave an example in terms of paths between two points; it is often the case that you care not only that the points are merely connected, but you also have a preference for which path is taken. Or, you can do an analysis of the paths themselves, and determine their length or average furthest distance from the nearest McDonalds. A path is "just" a proof of connectivity, but the individual paths can be quite distinct when studied themselves. Less abstractly, a constructive proof will yield an algorithm that can be performed, and we know quite well that the variety of sorting algorithms (that "merely" prove that "all lists are sortable") actually vary in quite important ways, including asymptotics and stability.

lupire 2y ago
Asymptotics and stability are different theorems. An algorithm is not a proof. It is a technique for proof. Two algorithms can be different, while not being meaningfully different profs that a list is sortable. To the extent that they are different, they proof different theorems, such as "list can be sorted in O(f) time" for an f of interest.
- Twisol 2y ago
  > An algorithm is not a proof. That is an opinion that many do not share. FWIW, I framed my response as an opinion; you gave yours as a blanket statement. It is not wrong to treat algorithms as valid proofs. In a dependent type theory, propositions are represented as types; the proposition that "all lists can be sorted" could be represented represented as the type "forall (t : Type) -> (le : Ordered t) -> forall (xs : List t) -> exists (ys : List t). (Increasing le ys, PermutationOf xs ys)". A proof of this proposition is exactly a program (algorithm) with that type; the sorted list is the `ys` component of the returned existential product. Yet the inhabitants of this type are not graded by asymptotics or stability; any sorting algorithm will do. In a setting where inhabitants of the above type are distinguishable, you could then write proofs of asymptotics or stability against individual algorithms. That is, the proofs of the sorting proposition are themselves the subjects of subsequent propositions and proofs thereof.

lupire 2y ago

A Proof is not a statement. A theorem is a statement. Proofs are usually not completely formal or even formalizable. Math is not completely well founded. "Unravelling it all the way" might be an open research project, or a new conjecture directly inspired by the second, apparently different proof. Showing these two profs to be equivalent might depend on a major new idea that happens after the two proofs are createdm This is hinted at in the OP discussion of Terry Tao.

bjornsing 2y ago
> Proofs are usually not completely formal or even formalizable. Math is not completely well founded. This is often stated, but is it really true? I haven’t seen a persuasive argument that not all math could (in principle) be formalized.

justinpombrio 2y ago

Some proofs that aren't "essentially the same": 1. Prove that the interior angles of a triangle sum to 180 degrees. First proof: draw a line parallel to one of the triangle's sides passing through its opposite vertex. There are three angles on one side of this line, and they obviously add to 180 degrees because it's a line. One of the three angles is directly one of the triangle's interior angles; the other two can be shown to be equal to the triangle's other two interior angles. (Try drawing it out.) Second proof: start at one side of the triangle and walk around it. By the time you return to where you started, you must have turned 360 degrees. Thus the sum of the exterior angles is 360 degrees. Each interior angle is 180 minus the corresponding exterior angle, and there are three of them, so calling the interior angles A, B, C and the exterior angles A', B', C' we have A'+B'+C' = 360 implies (180-A) + (180-B) + (180-C) = 360 implies 540 - A - B - C = 360 implies 180 = A + B + C. 2. Prove that the sum of the first N numbers is N(N+1)/2. First proof: sum the first and last number to get 1 + N, then the second and second-to-last to get 2 + (N-1) = 1 + N, repeating until you get to the middle. There are N/2 such pairs, giving a total of (1 + N)N/2. (This assumed that there were an even number of terms; consider the odd case too.) Second proof: proceed by induction. For the base case, it's true for N=1 because 1*2/2 = 1. For the inductive case, suppose it's true for N-1. Then 1 + 2 + ... + N-1 + N = (1 + 2 + ... + N-1) + N = N(N-1)/2 + N = N(N-1)/2 + 2N/2 = N(N+1)/2.

pkoird 2y ago
I'm responding to your second example simply because it's easy to argue about. I'd say that both proofs that you have presented are equivalent ways of saying that "since when you sum all the numbers from 1 to N you obtain a number that's N(N+1)/2, therefore, it is true that the sum of numbers from 1 to N is N(N+1)/2". Now, this argument may appear trite but do consider that both of your proofs essentially do the same thing with the first one summing the numbers from extremities and the second one summing 1...N-1 first and then the last. I'd argue that if addition were not commutative, you may have obtained different results.
- justinpombrio 2y ago
  If two programs are equivalent, you can typically show that they're equivalent with a sequence of small refactorings. Replace `x + x` with `2 * x`. Inline that function call. Etc. Can you do that with these two proofs? What's a proof that's halfway in between the two? If you can get from one proof to the other with small "refactorings", then I agree that they're fundamentally the same. If you can't---if there's an insurmountable gap that you need to leap across to transform one into the other---then I'd call them fundamentally different. If you insist that two proofs are "essentially the same thing" despite having this uncrossable gap between them, then I suspect you're defining "essentially the same" to mean "proves the same thing", which is a stupid definition because it makes all proofs the same by fiat, and avoids the interesting question.

Someone 2y ago

Theorem: there are 500,000 odd integers between zero and a million. Proof #1: there ar no odd integers between zero and 1 (inclusive), 1 is odd so there is 1 odd integer between zero and 2, 2 is even so there is 1 odd integer between zero and 3, 3 is odd so there are 2 odd integers between zero and 4, …, 999,998 is even so there are 499,999 odd integers between zero and 999,999, 999,999 is odd so there are 500,000 odd integers between zero and 1,000,000. QED. Proof #2: this is a specific case of “there are n odd integers between zero and 2n (exclusive)”. (proof of the more general theorem). Picking n to be 500,000, the theorem follows. I think most people would call those two proofs different.

winwang 2y ago

Two programs which are semantically equivalent are not simply the same. See: bubblesort vs mergesort. (Yes I'm relying on curry-howard isomorphism here).

andrewla 2y ago
I don't know why this hasn't been voted to the top. Curry-Howard isomorphism is a hell of a bludgeon to apply here but it makes for a very straightforward and obvious refutation of the parent post.

seanhunter 2y ago

I don't think this is true because a proof does more than state a conclusion. It establishes a true path from some premises to that conclusion. Sometimes that path continues. For example if you had a general constructive proof that there were infinitely many prime numbers it should be a simple matter to alter it a bit and prove the twin prime conjecture wouldn't it? In general a constructive proof and a non-constructive proof of some fact (say proof by contradiction) are fundamentally different in terms of where you can go with the proof.

naniwaduni 2y ago

> I'd argue that two correct proofs are always the same All correct inferences proceeding from the same axioms are the same.

tightbookkeeper 2y ago

No. Because the whole point of proof from a human perspective is to express understanding of the question, not merely answer it.

mjcohen 2y ago

How abut the following proofs that sqrt{2} is irrational. 1. If 2=a^2/b^2 with a and b relatively prime then a^2=2b^2 so a is even, and, letting a=2c, b is also even a contradiction. 2. Use the lemma that a positive real r is rational if and only if there is a positive integer b such that br is an integer. (Proof left to the reader.) if sqrt{2} is ration then there is an integer b such that bsqrt{2}=a for some integer a. Let b be the smallest such integer. Then, if c=b(sqrt{2}-1) then c is smaller than b, c=bsqrt{2}-b is an integer, and sqrt{2}c=sqrt{2}b(sqrt{2}-1)=2b-b*sqrt{2} is an integer, a contradiction (this uses infinite descent). 3. Use the theorem that if x, y, and n are positive integers such that x^2-ny^2=1 then sqrt{n} is irrational, and apply with n=2, x=3, y=2. Proof of theorem. a. If x^2-ny^2=1, then using (x^2-ny^2)^2=(x^2+ny^2)^2-n(2xy)^2 to show that there are arbitrarily large solutions to x^2-ny^2=1. b. If n=a^2/b^2 then 1=x^2-(a^2/b^2)y^2 so b^2=b^2x^2-a^2y^2=(bx+ay)(bx-ay)>=bx+ay>bx so b>x but this contradicts the existence of arbitrarily large x. How are any of these the same as any other?