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

equality27 × 37 = 999

This equality makes sense in the mainstream of mathematics by saying that the two sides

denotethe same integer and that × is afunctionin 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

computationprocess 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 × 37equals999, since if the two things we have werethe samethen we would never feel the need to state their equality. Concretely we ask aquestion, 27 × 37, and get ananswer, 999. The two expressions have differentsensesand we mustdosomething (make a proof or a calculation, or at least look in an encyclopedia) to show that these twosenseshave the samedenotation.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

finitarydynamics 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 tosyntacticmanipulation. This is nota prioriin 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 betweeninfinite, static denotationandfinite, 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 itssense, for example A ∨ B means "A or B", etc.

as the

ideal resultfound by these operations: this is itsdenotation."Denotation", as opposed to "notation", is what

is denoted, and not whatdenotes. 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).