Author Description

Abstract: "The two dynamic processes of proof theory, automated proof search and normalization, are studied. They are step-by-step, computational processes which at each step execute by performing a set of syntactical operations (such as erasing, copying). The syntactical operations arise from considerations concerning (a sharpening of) the subformula property. Different proof systems are discussed in light of the subformula property. Likewise, properties of automated proof search and normalization arising from the subformula property, are pointed out. Special attention is paid to linear logic because it may be seen as a concrete manifestation of several of the observations made. Based on this, a development along two strands is subsequently given. First, an account of computations basically consisting of the same set of syntactical operations is offered. From a computer science point of view, this amounts to simulating computations using the two aforementioned processes in proof theory; that is, to provide a rudimentary programming language. We provide two illustrations using linear logic: one modelling parallel computations (in CSP), the other the resource aware character of linear logic (in terms of the notion of 'wirings'). We argue that appreciated properties found in logic (such as permutability of rules, the Church- Rosser property of normalization) need not be equally desirable when devising programming languages in this manner. Second, the question of how meaning may be ascribed to the language of logic is addressed. The modern, intuitionistic position, stressing that a theory of meaning has to be grounded in the knowledge the reader and writer has of this meaning, is found to be especially rewarding. This knowledge is explicit or implicit - - the possession of a method or procedure for obtaining explicit. In the case of logic, the process of normalization has been suggested as approximating the required notion of method or procedure. We set out to assess t