Topics Logic

Question Logic textbooks which offer a system of natural deduction containing a so called "rule of replacement" restrict this rule to logically equivalent formulae. Only these can replace each other wherever they occur. I have often wondered why this is so. It seems to me that, having e.g. p<=>q and p&r as lines in a proof (as premisses, say), would allow one to soundly infer q&r directly from them by replacement of p by q in p&r, without requiring that p and r be logically equivalent. In less formal situations, for example, when solving a math problem, I find myself (and others) doing this all the time. I've searched the internet for this, but couldn't find any answer so far. Most grateful in advance for a reply.

Accepted:
August 13, 2008

Comments

The question of which supplementary rules to add officially to a logical system as "derived rules", over and above the introduction and elimination rules for the connectives, is largely a matter of taste, of how you weight trade-offs e.g. between ease of use and spartan elegance. There's a good review of the choices made in various texts by Jeff Pelletier here.

There's a need for some care here. In classical logic, one certainly does have the rule: From A <==> B and ...A..., infer ...B..., in the sense that the former things will always imply the latter thing, and also in the sense that, in any complete system, applications of this rule could always be replaced by applications of other rules. So, in such systems, this is what is sometimes called a "derived rule". But we do not always have this rule. Indeed, there are plenty of systems in which one does not have it. A simple example is a modal logic that has the additional operator ◊, meaning "possibly". It certainly does not follow from A <==> B and ◊A that ◊B. It does follow (at least in the usual systems) if A <==> B is not just true but a theorem.