A categorical equivalence of proofs.
Manfred E. Szabo · Notre Dame Journal of Formal Logic · 1974
Introduction.*An intuitionist proof of a sequent B -* A is essentially a "function," and in this paper we shall study certain properties of the class of such functions.In order to gain sufficient generality, we shall adopt a "multilinear" point of view and take a propositional subsystem of Gentzen's calculus LJ as a starting point.Gentzen's Hauptsatz states that for every provable sequent Γ -»A, the class [P] of LJ proofs of Γ -> A contains at least one cut-free representative.We can regard {P} as an equivalence class with respect to the relation E o on proofs in LJ defined by PE 0 Q iff Pand Q are proofs of the same sequent Γ-*A.The question which arises naturally in category theory is to what extent, if at all, E o can be refined to an equivalence relation E for a definite propositional fragment of LJ, denoted simply by < A, then PE Q iff P and Q are equi-general, where P and Q are equi-general, roughly speaking, if the terms in the initial sequents of P can be made as distinct as those in Q and conversely without destroying P and Q disproofs of the same sequent (but not necessarily of Γ -* A).(i) and (ii) will of course establish immediately certain invariance properties of well-known logical theorems, whereas an effective notion of "equi-generality" is needed in order to preserve the decidability of L.Whilst the questions raised in (i), (ii), and (iii) are of logical interest in their own right, the motivation for studying the particular deductive system L lies in the fact that L constitutes, as is easily deducible from *This paper was written while the author was a Visiting Fellow at St. Catherine's College, Oxford, and he wishes to express his thanks to the Fellows of St.