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)?
