Models of Deduction*

KOSTA DOSENMODELS OF DEDUCTION*ABSTRACT. In standard model theory, deductions are not the things one models.

But in general proof theory, in particular in categorial proof theory, one nds models

of deductions, and the purpose here is to motivate a simple example of such models.

This will be a model of deductions performed within an abstract context, where we

do not have any particular logical constant, but something underlying all logical

constants. In this context, deductions are represented by arrows in categories

involved in a general adjoint situation. To motivate the notion of adjointness, one of

the central notions of category theory, and of mathematics in general, it is rst

considered how some features of it occur in set-theoretical axioms and in the axioms

of the lambda calculus. Next, it is explained how this notion arises in the context of

deduction, where it characterizes logical constants. It is shown also how the categorial point of view suggests an analysis of propositional identity. The problem of

propositional identity, i.e., the problem of identity of meaning for propositions, is no

doubt a philosophical problem, but the spirit of the analysis proposed here will be

rather mathematical. Finally, it is considered whether models of deductions can

pretend to be a semantics. This question, which as so many questions having to do

with meaning brings us to that wall that blocked linguists and philosophers during

the whole of the twentieth century, is merely posed. At the very end, there is the

example of a geometrical model of adjunction. Without pretending that it is a

semantics, it is hoped that this model may prove illuminating and useful.1. INTRODUCTIONAccording to the traditional vocation of logic to study deductive

reasoning, deductions should indeed be of central concern to logicians. However, as an object of study, deductions have really a central place in a rather restricted area of logic called general proof theory

namely, proof theory done in the tradition of Gentzen. There, by

studying normalization of logical deductions, one is led to consider

criteria of identity of deductions. The goal of this brand of proof

theory might be to nd a mathematical answer to the philosophical

question What is deduction?, as recursion theory has found, with

much success, a mathematical answer to...