J. Y. Girard, et al. (1989). Proofs and types. Cambridge University Press, New York, NY, USA. (PDF)

I found introductory description of a number of ideas given in the beginning of this book very intuitively clear, and these ideas should be relevant to our discussion, preoccupied with the meaning of meaning as we are. Though the book itself is quite technical, the first chapter should be accessible to many readers.

From the beginning of the chapter:

Let us start with an example. There is a standard procedure for multiplication, which yields for the inputs 27 and 37 the result 999. What can we say about that?

A first attempt is to say that we have an equality

27 × 37 = 999

This equality makes sense in the mainstream of mathematics by saying that the two sides denote the same integer and that × is a function in the Cantorian sense of a graph.

This is the denotational aspect, which is undoubtedly correct, but it misses the essential point:

There is a finite computation process which shows that the denotations are equal. It is an abuse (and this is not cheap philosophy — it is a concrete question) to say that 27 × 37 equals 999, since if the two things we have were the same then we would never feel the need to state their equality. Concretely we ask a question, 27 × 37, and get an answer, 999. The two expressions have different senses and we must do something (make a proof or a calculation, or at least look in an encyclopedia) to show that these two senses have the same denotation.

Concerning ×, it is incorrect to say that this is a function (as a graph) since the computer in which the program is loaded has no room for an infinite graph. Hence we have to conclude that we are in the presence of a finitary dynamics related to this question of sense.

Whereas denotation was modelled at a very early stage, sense has been pushed towards subjectivism, with the result that the present mathematical treatment of sense is more or less reduced to syntactic manipulation. This is not a priori in the essence of the subject, and we can expect in the next decades to find a treatment of computation that would combine the advantages of denotational semantics (mathematical clarity) with those of syntax (finite dynamics). This book clearly rests on a tradition that is based on this unfortunate current state of affairs: in the dichotomy between infinite, static denotation and finite, dynamic sense, the denotational side is much more developed than the other.

So, one of the most fundamental distinctions in logic is that made by Frege: given a sentence A, there are two ways of seeing it:

• as a sequence of instructions, which determine its sense, for example A ∨ B means "A or B", etc.

• as the ideal result found by these operations: this is its denotation.

  "Denotation", as opposed to "notation", is what is denoted, and not what denotes. For example the denotation of a logical sentence is t (true) or f (false), and the denotation of A ∨ B can be obtained from the denotations of A and B by means of the truth table for disjunction.

Two sentences which have the same sense have the same denotation, that is obvious; but two sentences with the same denotation rarely have the same sense. For example, take a complicated mathematical equivalence A⇔B. The two sentences have the same denotation (they are true at the same time) but surely not the same sense, otherwise what is the point of showing the equivalence?

This example allows us to introduce some associations of ideas:

• sense, syntax, proofs;

• denotation, truth, semantics, algebraic operations.

That is the fundamental dichotomy in logic. Having said that, the two sides hardly play symmetrical roles!

Read the whole chapter (or the first three chapters). Download the book here (PDF).