The predicate of equality is supposed to represent formally the relation of identity which, in spite of its apparent triviality, was able to confuse even such prominent philosophers like Wittgenstein. It is difficult to find a serious application of logic without using this predicate. Equality is necessarynot only for the development of mathematical theories but plays also an important role in philosophical applications. Moreover, at least since Frege’sconsiderations, it is the source of many interesting philosophical and linguistic puzzles. The advent of non-classical logics strongly enlarged the spectrum of problems.

One of the interesting problems is the question whether equality is a logical constant or not. Clearly, the answer depends on the way we define the notion of logical constant. However, even if we think that there are important reasons for claiming that equality is a logical constant, it is problematic to show that it exhibits a behaviour similar to undisputable cases like extensional connectives or quantifiers.

In the tutorial we look at the problem from the proof-theoretic standpoint. After a survey of several ways of treating equality in formal systems of different sort we focus on the framework of sequent calculus (SC). This setting seems to be particularly well suited for investigations concerning the problems of criteria for logical constants and proof theoretic semantics. In the context of SC two proposals which were often discussed are those of Do˘sen [1] and Hacking [2]. Both will be examined in detail.

Another problem concerning equality and its proper treatment in SC is connected with rich languages introducing complex terms of different sorts. We focus on two strongly interrelated issues: formalization of the logic of definite descriptions, and modal predicate logic with rigid and nonrogid terms. The material is divided in the following way:

1. A Survey of Syntactical Approaches to Equality

In the first part we describe several ways of treating equality in formal systems of different sort, including natural deduction (ND) and tableaux. We focus on the framework of sequent calculus (SC) with the richest variety of solutions with equality characterised by means of sequents and rules of global or local character. These approaches will be discussed and compared from the standpoint of theoretical interest and practical utility.

2. Is Equality a Logical Constant?

Two variants of sequent calculus for classical logic will be examined, a structural and a logical one. The former is defined in accordance with Dosen’s criteria for logical constants. The latter resembles standard Gentzen’s sequent calculus and satisfies Hacking’s criteria for logicality. Both variants are provided in two versions; the first based on the standard notion of sequent and the second on the generalised one, with terms occuring on a par with formulae. It will be shown that the second approach provides better solution to the posed problem. In particular, whereas both versions satisfy Dosen’s criteria and provided rules are harmonious in some sense, only the second satisfies full cut elimination theorem which is one of the Hacking’s requirement.

References

[ [1] K. Dosen, "Logical constants as punctuation marks", Notre Dame Journal of Formal Logic, 30: 362–381, 1989.

[2] I. Hacking, "What is Logic?", The Journal of Philosophy, 76: 285–319, 1979.