3 ms·

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 l

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.

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.