#
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.

Read another response by Peter Smith, Richard Heck

Read another response about Logic