Home Philosophy Advances in Proof-Theoretic Semantics
Abstract We have a fresh look on Frege's mode of presentation, taking into account proofs of equalities as a key concept. Revisiting the classical example of Morning star and Evening star the account leads to a proposal for a proof-theoretic semantics of equalities.
Gottlob Frege opened his seminal paper Sinn und Bedeutung  by asking what the epistemic difference is between the equations a = a and a = b.1 His proposal to
distinguish between sense and denotation (or reference) of a term turned out to be one of the most fruitful conceptual advances in the history of philosophical logic.
Modern Possible Worlds Semantics draws on this distinction: the sense of a term refers to the full variety of possible worlds (in the way that we have to consider the denotation of a term in every possible world), while the (Fregean) denotation has to take into account only the actual world.
As appealing as this view might be, there are (at least) two problems with it. First, it comes with a concept of rigid designators. Second, it is not applicable to mathematics, because mathematical equations hold equally in every possible world.
While many approaches try to attack the problem from a semantic perspective, here we would like to provide a syntactic account, which takes up Frege's original question of the (epistemic2) difference of a = a and a = b. With restriction to singular terms, we will propose a fresh understanding of Frege's mode of presentation. It is motivated by the question how we actually prove a particular equation, and it can be considered as a proof-theoretic semantics of equalities.
To set the stage for the further discussion we would like to assume that we always use a first-order language for which we may have some non-logical axioms, and a fixed structure with universe A in which this language is interpreted3 by an interpretation function (•)M. Let us use Latin characters for terms of the language, and German
(Gothic) ones for elements of the structure. Equality is understood as the relation t = s on the syntactical level between terms of the first-order language4; identity stands for the (trivial) relation a ≡ a on the semantic level, which holds only between an object in the structure and itself.5 The fact that identity is not entirely trivial comes from its use for terms in combination with the interpretation in the form (t )M ≡ (s)M.6
In this setting we can recast Frege's first observation that “if we were to regard equality as a relation between that which the names 'a' and 'b' designate, it would seem that a = b could not differ from a = a (i.e. provided a = b is true). A relation
would thereby be expressed of a thing to itself, and indeed one in which each thing stands to itself but to no other thing.” [5, p. 157]. In our terminology we may say
that we are not concerned with the semantical identity relation a ≡ a, but with the syntactical equality relation t = s.
It is standard to axiomatize equality in first-order logic as a universal congruence relation, i.e., an equivalence relation compatible with all operations (functions and relations). As such, it mimics on the syntactic level just the properties which identity exhibits on the semantic level. But the domain of identity is simply A × A, and
the elements of A are unique in the sense that a ≡ a, but a /≡ b for two elements a, b ∈ A. On the syntactic side, however, the equality relation is defined for terms, and, clearly, two terms, though being interpreted by the same object a, may well be different.
Frege introduced the sense of a sign as its mode of presentation. Generally, this is taken as some kind of illustration rather than a definition. It is our aim to provide a more formal explication of mode of presentation by drawing on the difference of equality and identity.