In my previous post on Search for Mathematical Roots, I mentioned that one of the things that Frege complained about, according to Grattan-Guinness, was the overloading of symbols. I want to expand on that briefly in this post. I said that the same thing was done in proof theory. It seems that this is not completely accurate. The situation, from what I can tell from the Search for Mathematical Roots, was that often logicians, especially in the algebraic tradition, would use one symbol to designate many different things. For example, some would use ‘1’ to designate the universe of discourse as well as the truth-value true. The equals sign ‘=’ would do double duty as identity among elements as well as equivalence between propositions. It would also get used to indicate a definition. This would not be so bad, but often there would not be any clear way to tell what sense a sign would be used in, sometimes appearing in one sentence in multiple ways. Things get hairier when quantifiers are added, since the variables quantified over would sometimes be propositions and sometimes not.

How is this different than is the case in proof theory? In proof theory symbols are often overloaded in the sense that, in a sequent calculus, the symbol on the left means something different than on the right. Two examples are the comma, behaving conjunctively on the left and disjunctively on the right, and the empty sequence, acting as the true on the left and the false on the right. The difference between proof theory and the situation in the 19th century is that the overloading in proof theory is systematic. One can easily figure out what is going on based on its context. Not so with the algebraists. Grattan-Guinness, and Badesa, indicate different points in proofs in which a symbol slides from, say, a propositional interpretation to one that doesn’t have a clear propositional meaning. Often times, it seems, the logicians themselves did not make the distinctions and did not notice that they were slipping between the distinct senses. The overloading in proof theory is benign and useful whereas in the case of the 19th century algebraists it was confusing and sometimes hampered understanding.

Other examples are the signs for membership and set-inclusion, also things Frege harped on. Some logicians used membership and inclusion interchangeably. One reason Grattan-Guinness gives is that they were taking membership to be along the lines of the part-whole relationship of mereology, though he didn’t use the word “mereology.” While for some, this slip was due to unclarity about the concepts involved, this particular instance of overloading wasn’t seen as bad. Peano apparently was guilty of it, and Quine, in an article on Peano’s contributions to logic, said that he was right do so. One gets an interesting set theory, one Quine liked, if one doesn’t distinguish an element from its singleton, and so treating membership the same as single element inclusion.