A logician’s anomaly or: Leibniz vindicated

A logician's anomaly or: Leibniz vindicated

The following quotation is from "Cartesian closed categories and lambda calculus" by Gerard Huet, published as Chapter 2 in "Logical Foundations of Functional Programming", Gerard Huet (Ed.), (The UT Year of Programming Series), 1990, Addison-Wesley Publishing Company, Inc.:

This has an unfortunate consequence: The law of substitution of equals for equals does not hold whenever one replaces an expression containing a variable universally quantified over an empty domain with an expression not containing this variable, since we replace something which does not denote with something which may denote. For instance, consider the signature $H: A \to B$ , $T: B$ , $F: B$ , and the equations $H(x) = T$ and $H(x) = F$ . These equations are valid in the model where $A$ is the empty set, $H$ is the empty function, and $B$ is a set of two elements ${0, 1}$ , with $T$ interpreted as 1 and $F$ interpreted as 0. In this model we do not have $T = F$ . We shall have to keep this problem in mind in the following.

I was baffled! It is perfectly valid to derive

$$ (\underset {\sim} {A} x: x \in A: H (x) = T \land H (x) = F) \Rightarrow (\underset {\sim} {A} x: x \in A: T = F). $$

For $A = \varnothing$ , antecedent and consequent are both true. To "conclude" -as suggested - $T = F$ from the consequent is just an elementary error in predicate calculus. The consequent equivales

$$ T = F \quad v \quad A = \varnothing $$

and the error is no more and no less than the tacit assumption that the second disjunct is false. What has this mistake to do with Leib-

niz's Principle of "substitution of equals for equals"? Nothing, of course. But how, then, did Huet establish a link?

My, only explanation for his temptation to

$$ (A x: x \in A: H (x) = T \land H (x) = F) \Rightarrow T = F $$

is that universal quantification is not indicated explicitly but in the case of $H(x) = T$ and $H(x) = F$ is to be understood on account of the visible occurrence of the variable $x$ ; in $T = F$ , $x$ is no longer visible and hence the universal quantification over it is no longer understood! Is this the explanation? If so, Huet has given a striking example of the utter confusion inadequate notational conventions may generate. His introduction of somethings that do, do not, or may "denote" does not give much comfort either: to me it strongly suggests that his logic has not divorced itself from philosophy yet. Sometimes our logicians make it very difficult for us to take them seriously.

Austin, 23 September 1990

Prof. dr. Edsger W. Dgksha Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA