On Logic, Computation and Ideology

by David Pym

From The LFCS Newsletter, March 1991, Issue 3.

LOGIC, I LIKE TO SAY, is an itinerant subject: with its origins in Classical Philosophy, it is now of central importance in Computer Science. Having passed from the early mediæval, monastic tradition to the Philosophical Schools of the mediæval universities, most notably Paris, Logic experienced many centuries in which, with the exception of the (somewhat retrospectively) highly regarded work of the Scholastics, it was essentially dormant.

This Aristotelean tradition of the study of deduction expressed inference steps in natural language, but in 1879 came the publication of the Begriffsschrift [1] which for the first time provided a mathematically precise description - via the predicate calculus - of the notion of logical proof: with this work Frege at once provided a mechanism of enormous and essential mathematical interest - leading to what we now call Symbolic Logic - and an impetus for a new exploration of the relevance and application of Logical ideas to both the Mathematical and Moral Sciences [2,3]. This latter development has led to a great deal of work addressing the nature and objectives of the Scientific Method, and will not concern us further here.

After the Begriffsschrift the study of Symbolic Logic divided between the Mathematical and Philosophical schools of universities. Interactions between the two strands of development have been rather few, but of some significance in the development of the mathematical strand: for example, the study of Intuitionistic Logic on the one hand, and Modal Logic on the other, led Kripke et al. to develop possible worlds semantics [4]. Whilst this development is now losing favour in the philosophical strand, due largely to an appreciation of the value of Situated Logic [5] in Linguistics, in the mathematical strand the theory of Kripke models and toposes continues to expand in exciting ways. For example, recent work in Effective Domain Theory [6] seems to be of some significance for the semantics of programming languages.

In the mathematical tradition the disciplines of Model Theory, Recursion Theory and to a lesser extent Proof Theory began to be distinguished. Model Theory began to provide, with a very substantial degree of success, truth-functional analyses of logical consequence, with Gödel's Completeness Theorem [7] appearing in 1930. Proof Theory and Recursion Theory can be considered to have begun with Whitehead and Russell [8] and Gödel's Incompleteness Theorem [9].

A theory of computation can be considered to have begun in earnest in 1936 when Turing and Church independently provided precise analyses of the notion of abstract machine [10]. Note however that there was no serious notion of computer available at the time.

It was not until Herbrand's doctoral thesis, Recherches sur la théorie de la démonstration [11], which introduced several notions that were to be crucial in later work in Computational Logic, and Gentzen's Untersuchungen über das logische Schliessen [12], which introduced the notions of sequent and natural deduction that modern Proof Theory began to develop. For now not only were the proof-objects considered as entities of mathematical interest, but also the fine structural details of the process of their construction became a central object of investigation. In modern terms, the logical connectives were given an operational semantics. Thus modern Proof Theory can be considered to be the metatheoretic investigation of this operational semantics, just as Model Theory can be considered to be the metatheoretic investigation of the truth-functional semantics.

This step was crucial in the development not only of Logic, but also of Computation Theory - a term that neither Herbrand nor Gentzen would have recognised - for then it was possible to consider the relationship between the process of computation and the process of deduction. More than thirty years later, precise connections were identified by Howard [13] and Girard [14]. Now the relationship between lambda terms, computation and cut-elimination is clearer, though by no means settled. Indeed, one of the most exciting recent developments in Proof Theory, namely Linear Logic [15], is of some significance for computation theory in that it is inducing a more subtle analysis of these notions.

So from a logical point of view, what is (Theoretical) Computer Science? Certainly it is not concerned with the study of physical computing devices by means of the Scientific Method; such activities are properly those of Computer Engineers. Rather its concern is the mathematical theory sketched above. In particular, it is the precise mathematical logical analysis, via Proof Theory, Recursion Theory, Model Theory and Computation Theory, of the actions of suitable abstract notions of machine, and the study of the relationship between these notions and (other) cognitive sciences, as well as computer engineering. Such an analysis proceeds in two principal directions. One is the consideration of direct implementations of logical notions; for example. Prolog's resolution rule is composed of the cut rule together with unification - a notion that was present, implicitly, in Herbrand's thesis. The other is the mathematical logical characterisation of more linguistically and mechanically motivated ideas; for example, the denotational semantics of imperative programming languages and languages for discussing abstract notions of process, such as the pi-calculus of Milner et al.

What is the status of real computers? I contend that (Theoretical) Computer Science) should require that computer be nothing more than physical devices that finitely approximate our abstract notion of machine, provided the nature of that approximation is precisely specified in any given instance. For example, when reasoning about the behaviour of hardware, one should assume that components fail according to given probability distribution.

From the point of view of the cognitive sciences more generally, a situated [16] analysis of the rôle and status of computers is probably appropriate, but a discussion of such ideas is beyond the scope of this note.

I conclude by stating that whilst I hope to develop an extended article along these lines, I consider this note to be merely a preliminary cartoon. Also, I observe that writing history is rather difficult.