Recent searches
Search options
Of 111 people who answered the question "are logically equivalent statements entirely interchangeable in every situation" https://mathstodon.xyz/@andrejbauer/112881057575938533, 38% answered affirmatively and 62% negatively.
I have found it to be a misconception both by students and mathematicians that A ⇔ B makes A and B "totally the same thing". But this is very much not the case!
As @MartinEscardo quipped, if a statement could always be replaced with an equivalent one, one could take a paper and replace all theorems with "True". They are all equivalent to true after all.
Speaking a bit more formally, a statement can be exchanged with an equivalent one so long as we are only concerned with their truth values. However, once we start paying attention to proofs, it becomes clear that the precise form of a statement matters in some situations. A proof p of statement A only becomes a valid proof of an equivalent statement B once we *transport* p along the proof e of equivalence A ⇔ B.
In fact, this sort of phenomenon happens more generally: an element p of a structure A is not itself an element of an isomorphic structure B, but must be mapped to the corresponding element e(p) by an isomorphism e : A → B. Which element we get may depend on which isomorphism e we pick.
Bonus puzzle: which proof of Infinitude of primes do you get if you transport a proof of Pythagoras's theorem along a proof of equivalence "Pythagoras's theorem ⇔ Infinifude of primes"?
(If you are itching to expose the subliminal messages in this post, please don't and just enjoy the fact that you know what my ulterior motives are.)
@andrejbauer @MartinEscardo
What proof systems allow to transport proofs along equivalences (without any additional input of the user)?
@antoinechambertloir @andrejbauer
E.g. in HoTT/UF.
Transport along logically equivalent propositions is used often in TypeTopology.
This is called propositional extensionality, and is a special case of univalence.
In one case I use it a lot because I originally adopted one definition, but it turned out that another, logically equivalent, definition was often more convenient.
In one extreme case, I even replaced a theorem by "True" to make a proof simpler:
https://www.cs.bham.ac.uk/~mhe/TypeTopology/CantorSchroederBernstein.CSB.html#ulemma
@andrejbauer @MartinEscardo @jonmsterling something something frege something something hesperus something phosphorus
@andrejbauer @MartinEscardo I got confused about this very distinction earlier this week, so thanks for the exposition!
@rg9119 @andrejbauer @MartinEscardo does this coincide with what people mean when they talk about "proof relevance" in a colloquial sense (I'm aware of the different formulations of proof relevance Andrej has articulated elsewhere, but curious how the general treatment in this post fits into those definitions)