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.


Let $(R\implies (\neg P\land S\implies T))$ be $S_P.$

Let $(R\implies (\neg Q\land S\implies T))$ be $S_Q.$

  1. $P\iff Q$ Premise
  2. $R\implies (\neg P\land S\implies T)$ Premise
  3. $S_P\land (P\iff Q))\implies S_Q$ Logical Truth (Tautology)
  4. $S_P\land (P\iff Q))$ Adjunction (2)(1)
  5. $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.

  • $\begingroup$ I agree with your reasoning that replacement instances can be proved from $P\iff Q$. How do you define logically equivalent? (What's an example of biconditional statements that are not logically equivalent?) $\endgroup$
    – Karl
    Commented May 20, 2023 at 1:57
  • 2
    $\begingroup$ "I ask because there has been many proofs where it would have saved lots of time using a replacement from a biconditional, rather than deduce the same sentence step-by-step." It might be good to include such an example in your question. $\endgroup$
    – Chris
    Commented May 20, 2023 at 2:06
  • 1
    $\begingroup$ Your recent edit hasn't explained what the more limited notion of "logically equivalent" that you're using is. I'd consider $P$ and $Q$ logically equivalent if $P\iff Q$ is provable. $\endgroup$
    – Karl
    Commented May 20, 2023 at 7:32
  • $\begingroup$ Your purported "proof" sounds like: "if $0=1$, then $0+0=2$". This is not a proof of $0+0=2$. $\endgroup$ Commented May 20, 2023 at 12:20
  • $\begingroup$ @Karl I edited it. I asked about the distinction from here, so here is a link to that post. math.stackexchange.com/q/4652840/1067915 $\endgroup$ Commented May 20, 2023 at 14:40

1 Answer 1


Your reasoning about replacement is correct! I think the answers you got on the linked question are a little misleading for your purposes. Logical equivalence in the strict sense used there depends on which rules/definitions/axioms you consider fixed and which ones you allow to vary when considering alternative models; the counterexamples given are based on models where symbols like + have been given nonstandard meanings (treating only the logic symbols as fixed since we want logical equivalence). These examples reflect the fairly obvious fact that if my "+" means something different from your "+", then your proof of a statement involving + is invalid to me (unless you proved something like $x=y\implies x+x=y+y$, using only the syntactic form of +).

When doing math in practice, we're only interested in models that satisfy our definitions and axioms (about the properties of sets, numbers, etc.), and when you prove $P\iff Q$ from those definitions and axioms, you are proving that $P$ and $Q$ have the same truth value in every such model. This justifies substituting one for the other in any expression. (The only models where the substitution fails are ones that reinterpret the symbols of your language in a way that violates your definitions/axioms, and the whole point of establishing and using definitions/axioms is to exclude those models from consideration.)


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .