I've always wondered whether biconditional statements that are not logically equivalent validly replace each other in bigger sentences, on the basis that since they must have the same truth values therefore every sentence that they are in should have the same truth values.
It seems that with enough rules of inference in a proof, you can always end up with a "replacement": if I have $(P\iff Q)$ and a sentence $S_P$ with subsentence $P,$ then the sentence $S_Q$ with subsentence $Q$ can always be deduced.
Example
Let $(R\implies (\neg P\land S\implies T))$ be $S_P.$
Let $(R\implies (\neg Q\land S\implies T))$ be $S_Q.$
- $P\iff Q$ Premise
- $R\implies (\neg P\land S\implies T)$ Premise
- $S_P\land (P\iff Q))\implies S_Q$ Logical Truth (Tautology)
- $S_P\land (P\iff Q))$ Adjunction (2)(1)
- $S_Q$ Modus Ponendo Ponens (3)(4)
It seems this would work no matter what $S_P$ is. But if this were the case, then why is "replacement" always limited to logically equivalent sentences?
I ask because there has been many proofs where it would have saved lots of time using a replacement from a biconditional, rather than deducing the replacement sentence step-by-step.
I've been told that two sentences are logical equivalent if and only if they have the same truth values in every model. So, while 1+1=2⟺99+1=100 is a true biconditional, assuming we are speaking about arithmetic, in a different model 1, 2, +, 99, and 100 could be defined differently, giving a different truth value to the sentence.