Equivalence

BicycleTree

I've wondered about this. The book for my logic course (now done with) had no rule for creating equivalences. If you had A <--> B, by the system in the book you couldn't replace occurrences of A with B and occurrences of B with A. You'd have to break down A <--> B with material equivalence and work from there.

Is there any particular reason for that?

honestrosewater

You're talking about a natural deduction system? I think it may take several rules to state. The English statement would be something like, "If P and Q are equivalent, then you can replace any occurence of P with Q and any occurence of Q with P." Right? So this would be an inference rule (and I don't see how you could state it as a replacement rule). I don't see anyway to translate "any occurence of P" and "any occurence of Q" into a single rule. It seems you would need an inference rule for each type of proposition in which P or Q could occur. For instance, one rule would be
(P <-> Q)
(P -> R)
.: (Q -> R)
but you would need a different rule for when P occurs as the consequent, when P occurs in a conjunction, etc. You may also need another commutation rule for equivalences [(P <-> Q) <=> (Q <-> P)]. I don't know, I'm not quite awake yet. Does that make sense to you?

BicycleTree

No, you could say it similar to how instantiation and generalization rules are stated for predicate logic. "If P <--> Q and S(Q) is a statement containing at least one instance of Q and S(Q) appears on some line, then S(P), a statement replacing one or more instances of Q in S(Q) with P, can be inferred." Rules don't have to be stated in the language of the inference system; they just have to be stated clearly so that they can be applied in the inference system.