6 ms·

When are two proofs essentially the same? (2007)

72 points by ColinWright 2y ago

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?
lupire 2y ago
> A couple of years ago I spoke at a conference about mathematics that brought together philosophers, psychologists and mathematicians. The proceedings of the conference will appear fairly soon Can we do better?
- drpossum 2y ago
  [flagged]
- glitchc 2y ago
  Not for free we can't.
- deleted 2y ago
  [deleted]
Xcelerate 2y ago
One way to compare proofs is to consider whether they belong to the same "level" or not. Consider by analogy whether a particular Turing machine halts. You can look at the sequence of configurations of the Turing machine at each step. Since the evolution of the machine's configuration is deterministic, any configuration along a "halting path" ends up in the same final configuration (i.e., the first configuration in a halting state). But that's too difficult in some cases. Most of the Goodstein sequences reach extraordinarily high values before coming back down. How can we prove they all eventually reach 0? Even at small values of n, the sequence length of G(n) requires something on the order of the Ackermann function to specify bounds. We can't inspect these sequences directly to prove whether they reach 0. Instead we create a "parallel" sequence to a Goodstein sequence. Then we prove there exists an algorithm that maps from each item in the parallel sequence to an item in the Goodstein sequence such that both sequences are well-ordered and decreasing. If the parallel sequence reaches 0, then so does the Goodstein sequence. You could think of this as one Turing machine computing the configurations of another Turing machine or perhaps one branch of a tree "cross-predicting" the items along another branch. You aren't just following the branch to its end. In this sense, the proof occurs at a higher "level". This concept is known as ordinal analysis and one can consider the proof-theoretic ordinal of any theory T. If T_1 and T_2 both prove a specific theorem and have the same proof-theoretic ordinal, you could consider the two proofs to occur on the same "level". Interestingly, Peano Arithmetic can prove that any specific Goodstein sequence reaches 0 but not that all Goodstein sequences reach 0—this requires a more powerful formal system. So if you prove a specific sequence reaches 0 using the more powerful system, I would say that's a fundamentally different proof.
- colechristensen 2y ago
  >I agree with pkoird's point that philosophically, two correct proofs of the same theorem should be considered "the same". Any theorem is ultimately a property of the natural numbers themselves along with the various paths that lead there from the axioms (since all proofs are essentially a finite sequence of Gödel numbers). As with a lot of philosophy, the argument turns out to actually be much more about defining terms being used than the objects those terms are referring to. I mean when you are making an argument about "x is the same as y because..." your philosophical argument is actually about what should be meant by the same instead of any particular properties of x or y. The article seems to be digging at the existence of a few categories of proofs * proofs that are trivially transformed into one another * proofs that use substantially similar arguments that don't necessary have a direct transformation * proofs that arrive at the same destination through a much different path that have no obvious transformation to another proof So the question is: how easy does it have to be to transform one proof to another in order for them to be considered "the same"? One extreme is "the slightest change in wording makes a proof unique" The other extreme is "any two proofs of the same concept are by definition the same proof" I would argue that neither extreme is particularly useful, because both are just obvious. One means "these are different sheets of paper" and the other means "these are both proofs of X", neither of which are interesting statements. What is an interesting statement is commentary on the path made to a proof and the differences in paths to proving a statement. Both in the ability to transform one into another easily to show similarity, and in the difficulty to transform one into another to show divergence.
jkaptur 2y ago
I'm reminded of the Philosophy of Computer Science entry in the Stanford Encyclopedia of Philosophy [0], which briefly considers what it means for two programs to be identical. "... it has been argued that there are cases in which it is not possible to determine whether two programs are the same without making reference to an external semantics. Sprevak (2010) proposes to consider two programs for addition which differ from the fact that one operates on Arabic, the other one on Roman numerals. The two programs compute the same function, namely addition, but this cannot always be established by inspecting the code with its subroutines; it must be determined by assigning content to the input/output strings" "The problem can be tackled by fixing an identity criterion, namely a formal relation, that any two programs should entertain in order to be defined as identical. Angius and Primiero (2018) show how to use the process algebra relation of bisimulation between the two automata implemented by two programs under examination as such an identity criterion. Bisimulation allows to establish matching structural properties of programs implementing the same function, as well as providing weaker criteria for copies in terms of simulation." (Of course, it isn't surprising that this would be relevant, because proofs and programs themselves are isomorphic). This technique seems rather stricter than what Gowers has in mind, but it seems helpful as a baseline. 0. https://plato.stanford.edu/entries/computer-science/ https://plato.stanford.edu/entries/computer-science/
- chongli 2y ago
  I think it's also important to make a distinction between a pair of programs which compute the same function using an identical amount of space and time and a pair of programs which compute the same function with different amounts of either space or time (or both). Two programs might compute the same function and be considered formally identical in that sense but may be in radically different complexity classes [O(1) vs O(n) vs O(n^2) vs O(2^n)]. Formally we may not be interested in this distinction but practically we definitely are. One program may be extremely practical and useful whereas the other might not finish computing anything before the heat death of the universe on anything but trivial-sized inputs.
  - setopt 2y ago
    On the other hand, compiler tricks like tail call optimization can e.g. reduce an O(n) algorithm to an O(1) algorithm. Is it a “different program” if the same source code is compiled with a new compiler?
VikingCoder 2y ago
I was working with a friend writing a paper about the Ship of Theseus, but my friend kept replacing all of my arguments.
- lisper 2y ago
  I had a similar experience, but my collaborator had a touch of OCD and just kept micro-editing my original draft, each time replacing exactly one word with a different word that had nearly the same meaning. By the end of the process, my collaborator had produced a word-for-word copy of William Shakespeare's "Julius Caesar". It is a remarkable coincidence that my original draft just happened to have the same number of words to begin with to make this transformation possible. My collaborator then translated the original paper into Greek. Or maybe he translated "Julius Caesar" into Greek. I don't speak Greek so I have no way of knowing. ;-)
  - lanstin 2y ago
    I assume this is a joke related to Borges' don Quixote story? https://news.ycombinator.com/item?id=19143496 https://news.ycombinator.com/item?id=19143496
    - lisper 2y ago
      It is a joke, but not related to Borges, at least not intentionally.
  - js8 2y ago
    Ahh, the language diffusion model! You start with a word salad and end up with a Shakespeare's play.
082349872349872 2y ago
See Girard, The Blind Spot: Lectures on Logic (2011) for some attempts at tackling this question. (in particular, his "proof nets" attempt to have a canonical form, such that we can identify differently drawn concrete proof nets as representing the same abstract proof) https://en.wikipedia.org/wiki/Proof_net https://en.wikipedia.org/wiki/Proof_net
throwaway81523 2y ago
See: https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_problem https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_prob... https://mathoverflow.net/questions/3776/when-are-two-proofs-of-the-same-theorem-really-different-proofs https://mathoverflow.net/questions/3776/when-are-two-proofs-...
joe_the_user 2y ago
Well, if you define a proof system as a series of potential manipulations of a space of true statements, a given proof is a sequence of manipulations and states and thus a path in a sort-of-metric space. Two proofs could said to be similar if their paths are "close" in that sort-of-metric space. Of course, you're left with the question of how close is close and whether "close" means close at one intermediate point or many. Moreover, mathematicians often like proofs that are more "cohesive" than just sequences of manipulations. So the question with real world would probably be a matter of mathematical taste as well as objective measures.
- setopt 2y ago
  It’s also hard to prove that a statement definitely lies in the “space of true statements”. Moreover, whether a proof assumes “A = B” or “B = C” can make them closer together or further apart in such a space depending on whether it is established that “A = C” or not, which also makes it tricky to establish rigorously.
  - chongli 2y ago
    If you haven’t established that A = B and B = C implies A = C then you haven’t proven that = is an equivalence relation on that space including A, B, and C. Unless you’re going to prove it I would go so far as to call it an abuse of notation to continue using = when you mean some other relation where transitivity does not necessarily hold.
    - setopt 2y ago
      What I mean is that at the time something is proven, it might not be clear that those assumptions are equivalent. Like assuming at the start of a proof that the Axiom of Choice holds vs that Zorn’s lemma holds. That those two proofs are “close” requires that you know it’s already proven that they are equivalent. In that sense, I believe whether proofs should be considered close or not is more subjective than objective, as it depends on the previous knowledge of the reader. My point above is that one mathematician might assume A=B and another might assume A=C, and both prove the same things. That doesn’t mean they know that always B=C even if it’s true, in which case it’s hard to say whether the proofs are close.
SkiFire13 2y ago
> For example, it is often possible to convert a standard inductive proof into a proof by contradiction I would not consider those the same though, as one is constructive and the other is not.
WCSTombs 2y ago
> Is it ever possible to give a completely compelling argument that two proofs are genuinely different? I think in some cases, we can. Sometimes one of the proofs generalizes better than the other because it uses strictly fewer assumptions. It seems fair to say those would have to be inequivalent.
qubitly 2y ago
Reducing two mathematical proofs to being 'essentially the same' just because they reach the same conclusion overlooks something crucial: each proof isn’t merely a path to a result but a unique expression of understanding. A proof has its own logical and conceptual structure, and that structure isn’t interchangeable without losing some of its inherent value. Comparing proofs shouldn’t just focus on a shared outcome: the path taken, the relationships it establishes, and the concepts it explores are as fundamental as the conclusion itself. Perhaps it’s time to view mathematics not just as calculation, but as a real act of knowledge that in its diversity deepens our grasp of reality
- red_trumpet 2y ago
  The result of a prove is a theorem. I don't see any claim in the article that any two proofs of the same theorem are essentially the same?
- smfjaw 2y ago
  computational reducibility/irreducibility is a big topic in computer science and is incredibly interesting. It allows us to prove that certain "computers" are the same through proofs and that they can carry out the same tasks regardless of the actions that take place within them. I would suggest looking into that as it really opens your eyes to just how similar computationally so many things are
- samatman 2y ago
  But where is the line? Proof A and Proof A' are identical, except that Proof A says "and therefore" where Proof A' says "and so we see that". Different proofs? Proof A'' is a faithful translation of Proof A into French, is it now different? Or is it a trivial translation of the same proof into different language? This is, in fact, the topic of the Fine Article. The layman (myself included) sees easily that proof is something more durable than the exact words chosen, or even the language the proof is written in. Mathematicians (and patzers such as yours truly) will tend to view trivial transformations of a step in a proof, or trivially equivalent tactics, as resulting in the same proof. What makes such a transformation trivial? Good question.
deleted 2y ago
[deleted]
deleted 2y ago
[deleted]
deleted 2y ago
[deleted]

72 points by ColinWright 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?

lupire 2y ago

> A couple of years ago I spoke at a conference about mathematics that brought together philosophers, psychologists and mathematicians. The proceedings of the conference will appear fairly soon Can we do better?

drpossum 2y ago
[flagged]
glitchc 2y ago
Not for free we can't.
deleted 2y ago
[deleted]

Xcelerate 2y ago

One way to compare proofs is to consider whether they belong to the same "level" or not. Consider by analogy whether a particular Turing machine halts. You can look at the sequence of configurations of the Turing machine at each step. Since the evolution of the machine's configuration is deterministic, any configuration along a "halting path" ends up in the same final configuration (i.e., the first configuration in a halting state). But that's too difficult in some cases. Most of the Goodstein sequences reach extraordinarily high values before coming back down. How can we prove they all eventually reach 0? Even at small values of n, the sequence length of G(n) requires something on the order of the Ackermann function to specify bounds. We can't inspect these sequences directly to prove whether they reach 0. Instead we create a "parallel" sequence to a Goodstein sequence. Then we prove there exists an algorithm that maps from each item in the parallel sequence to an item in the Goodstein sequence such that both sequences are well-ordered and decreasing. If the parallel sequence reaches 0, then so does the Goodstein sequence. You could think of this as one Turing machine computing the configurations of another Turing machine or perhaps one branch of a tree "cross-predicting" the items along another branch. You aren't just following the branch to its end. In this sense, the proof occurs at a higher "level". This concept is known as ordinal analysis and one can consider the proof-theoretic ordinal of any theory T. If T_1 and T_2 both prove a specific theorem and have the same proof-theoretic ordinal, you could consider the two proofs to occur on the same "level". Interestingly, Peano Arithmetic can prove that any specific Goodstein sequence reaches 0 but not that all Goodstein sequences reach 0—this requires a more powerful formal system. So if you prove a specific sequence reaches 0 using the more powerful system, I would say that's a fundamentally different proof.

colechristensen 2y ago
>I agree with pkoird's point that philosophically, two correct proofs of the same theorem should be considered "the same". Any theorem is ultimately a property of the natural numbers themselves along with the various paths that lead there from the axioms (since all proofs are essentially a finite sequence of Gödel numbers). As with a lot of philosophy, the argument turns out to actually be much more about defining terms being used than the objects those terms are referring to. I mean when you are making an argument about "x is the same as y because..." your philosophical argument is actually about what should be meant by the same instead of any particular properties of x or y. The article seems to be digging at the existence of a few categories of proofs * proofs that are trivially transformed into one another * proofs that use substantially similar arguments that don't necessary have a direct transformation * proofs that arrive at the same destination through a much different path that have no obvious transformation to another proof So the question is: how easy does it have to be to transform one proof to another in order for them to be considered "the same"? One extreme is "the slightest change in wording makes a proof unique" The other extreme is "any two proofs of the same concept are by definition the same proof" I would argue that neither extreme is particularly useful, because both are just obvious. One means "these are different sheets of paper" and the other means "these are both proofs of X", neither of which are interesting statements. What is an interesting statement is commentary on the path made to a proof and the differences in paths to proving a statement. Both in the ability to transform one into another easily to show similarity, and in the difficulty to transform one into another to show divergence.

jkaptur 2y ago

I'm reminded of the Philosophy of Computer Science entry in the Stanford Encyclopedia of Philosophy [0], which briefly considers what it means for two programs to be identical. "... it has been argued that there are cases in which it is not possible to determine whether two programs are the same without making reference to an external semantics. Sprevak (2010) proposes to consider two programs for addition which differ from the fact that one operates on Arabic, the other one on Roman numerals. The two programs compute the same function, namely addition, but this cannot always be established by inspecting the code with its subroutines; it must be determined by assigning content to the input/output strings" "The problem can be tackled by fixing an identity criterion, namely a formal relation, that any two programs should entertain in order to be defined as identical. Angius and Primiero (2018) show how to use the process algebra relation of bisimulation between the two automata implemented by two programs under examination as such an identity criterion. Bisimulation allows to establish matching structural properties of programs implementing the same function, as well as providing weaker criteria for copies in terms of simulation." (Of course, it isn't surprising that this would be relevant, because proofs and programs themselves are isomorphic). This technique seems rather stricter than what Gowers has in mind, but it seems helpful as a baseline. 0. https://plato.stanford.edu/entries/computer-science/ https://plato.stanford.edu/entries/computer-science/

chongli 2y ago
I think it's also important to make a distinction between a pair of programs which compute the same function using an identical amount of space and time and a pair of programs which compute the same function with different amounts of either space or time (or both). Two programs might compute the same function and be considered formally identical in that sense but may be in radically different complexity classes [O(1) vs O(n) vs O(n^2) vs O(2^n)]. Formally we may not be interested in this distinction but practically we definitely are. One program may be extremely practical and useful whereas the other might not finish computing anything before the heat death of the universe on anything but trivial-sized inputs.
- setopt 2y ago
  On the other hand, compiler tricks like tail call optimization can e.g. reduce an O(n) algorithm to an O(1) algorithm. Is it a “different program” if the same source code is compiled with a new compiler?

VikingCoder 2y ago

I was working with a friend writing a paper about the Ship of Theseus, but my friend kept replacing all of my arguments.

lisper 2y ago
I had a similar experience, but my collaborator had a touch of OCD and just kept micro-editing my original draft, each time replacing exactly one word with a different word that had nearly the same meaning. By the end of the process, my collaborator had produced a word-for-word copy of William Shakespeare's "Julius Caesar". It is a remarkable coincidence that my original draft just happened to have the same number of words to begin with to make this transformation possible. My collaborator then translated the original paper into Greek. Or maybe he translated "Julius Caesar" into Greek. I don't speak Greek so I have no way of knowing. ;-)
- lanstin 2y ago
  I assume this is a joke related to Borges' don Quixote story? https://news.ycombinator.com/item?id=19143496 https://news.ycombinator.com/item?id=19143496
  - lisper 2y ago
    It is a joke, but not related to Borges, at least not intentionally.
- js8 2y ago
  Ahh, the language diffusion model! You start with a word salad and end up with a Shakespeare's play.

082349872349872 2y ago

See Girard, The Blind Spot: Lectures on Logic (2011) for some attempts at tackling this question. (in particular, his "proof nets" attempt to have a canonical form, such that we can identify differently drawn concrete proof nets as representing the same abstract proof) https://en.wikipedia.org/wiki/Proof_net https://en.wikipedia.org/wiki/Proof_net

throwaway81523 2y ago

See: https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_problem https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_prob... https://mathoverflow.net/questions/3776/when-are-two-proofs-of-the-same-theorem-really-different-proofs https://mathoverflow.net/questions/3776/when-are-two-proofs-...

joe_the_user 2y ago

Well, if you define a proof system as a series of potential manipulations of a space of true statements, a given proof is a sequence of manipulations and states and thus a path in a sort-of-metric space. Two proofs could said to be similar if their paths are "close" in that sort-of-metric space. Of course, you're left with the question of how close is close and whether "close" means close at one intermediate point or many. Moreover, mathematicians often like proofs that are more "cohesive" than just sequences of manipulations. So the question with real world would probably be a matter of mathematical taste as well as objective measures.

setopt 2y ago
It’s also hard to prove that a statement definitely lies in the “space of true statements”. Moreover, whether a proof assumes “A = B” or “B = C” can make them closer together or further apart in such a space depending on whether it is established that “A = C” or not, which also makes it tricky to establish rigorously.
- chongli 2y ago
  If you haven’t established that A = B and B = C implies A = C then you haven’t proven that = is an equivalence relation on that space including A, B, and C. Unless you’re going to prove it I would go so far as to call it an abuse of notation to continue using = when you mean some other relation where transitivity does not necessarily hold.
  - setopt 2y ago
    What I mean is that at the time something is proven, it might not be clear that those assumptions are equivalent. Like assuming at the start of a proof that the Axiom of Choice holds vs that Zorn’s lemma holds. That those two proofs are “close” requires that you know it’s already proven that they are equivalent. In that sense, I believe whether proofs should be considered close or not is more subjective than objective, as it depends on the previous knowledge of the reader. My point above is that one mathematician might assume A=B and another might assume A=C, and both prove the same things. That doesn’t mean they know that always B=C even if it’s true, in which case it’s hard to say whether the proofs are close.

SkiFire13 2y ago

> For example, it is often possible to convert a standard inductive proof into a proof by contradiction I would not consider those the same though, as one is constructive and the other is not.

WCSTombs 2y ago

> Is it ever possible to give a completely compelling argument that two proofs are genuinely different? I think in some cases, we can. Sometimes one of the proofs generalizes better than the other because it uses strictly fewer assumptions. It seems fair to say those would have to be inequivalent.

qubitly 2y ago

Reducing two mathematical proofs to being 'essentially the same' just because they reach the same conclusion overlooks something crucial: each proof isn’t merely a path to a result but a unique expression of understanding. A proof has its own logical and conceptual structure, and that structure isn’t interchangeable without losing some of its inherent value. Comparing proofs shouldn’t just focus on a shared outcome: the path taken, the relationships it establishes, and the concepts it explores are as fundamental as the conclusion itself. Perhaps it’s time to view mathematics not just as calculation, but as a real act of knowledge that in its diversity deepens our grasp of reality

red_trumpet 2y ago
The result of a prove is a theorem. I don't see any claim in the article that any two proofs of the same theorem are essentially the same?
smfjaw 2y ago
computational reducibility/irreducibility is a big topic in computer science and is incredibly interesting. It allows us to prove that certain "computers" are the same through proofs and that they can carry out the same tasks regardless of the actions that take place within them. I would suggest looking into that as it really opens your eyes to just how similar computationally so many things are
samatman 2y ago
But where is the line? Proof A and Proof A' are identical, except that Proof A says "and therefore" where Proof A' says "and so we see that". Different proofs? Proof A'' is a faithful translation of Proof A into French, is it now different? Or is it a trivial translation of the same proof into different language? This is, in fact, the topic of the Fine Article. The layman (myself included) sees easily that proof is something more durable than the exact words chosen, or even the language the proof is written in. Mathematicians (and patzers such as yours truly) will tend to view trivial transformations of a step in a proof, or trivially equivalent tactics, as resulting in the same proof. What makes such a transformation trivial? Good question.

deleted 2y ago

[deleted]

deleted 2y ago

[deleted]

deleted 2y ago

[deleted]