ABSTRACT
Modern formal logic was developed by mathematicians and its first applications were to problems in the foundations of mathematics. As the reader probably recalls, with or without nostalgia, elementary mathematical reasoning typically involves substituting equals for equals in equations, the simplest example of which is as follows:
We usually regard (1) as a valid deductive inference. Here we seem to have a problem, however, for=would normally be formalised by a binary relation symbol R, transforming (1) into
But this inference is certainly not valid in first-order logic, for the tree
is finished and open! Therefore the inference is invalid. So why do we nevertheless regard it as deductively valid?
