Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Coherence for logicians

Zoran Petric, Mladen Zekic

Abstract

This paper is addressed to logicians not familiar with category theory. It gives a new proof of coherence for symmetric monoidal closed categories, proven by Kelly and Mac Lane in early 1970s. We find this result of great importance for proof theory and it is formulated here in pure logical terminology free of categorial notions. Coherence is related to the generality conjecture in general proof theory and we hope that our formulation will make it closer to the proof-theoretical community.

Coherence for logicians

Abstract

This paper is addressed to logicians not familiar with category theory. It gives a new proof of coherence for symmetric monoidal closed categories, proven by Kelly and Mac Lane in early 1970s. We find this result of great importance for proof theory and it is formulated here in pure logical terminology free of categorial notions. Coherence is related to the generality conjecture in general proof theory and we hope that our formulation will make it closer to the proof-theoretical community.
Paper Structure (7 sections, 25 theorems, 105 equations, 1 figure)

This paper contains 7 sections, 25 theorems, 105 equations, 1 figure.

Table of Contents

  1. Introduction
  2. The system S
  3. Two propositions about derivability in $\mathcal{S}$
  4. The system IL
  5. The main result
  6. An application of the main result
  7. An elementary dictionary of category theory

Key Result

Lemma 2.2

If $A$ is a constant formula, then $A\vdash I$ and $I\vdash A$ are derivable in $\mathcal{S}$.

Figures (1)

  • Figure 1: Links in a term

Theorems & Definitions (65)

  • Remark 2.1
  • Definition 2.1
  • Lemma 2.2
  • Corollary 2.3
  • Theorem 2.4: Cut-elimination
  • Definition 2.2
  • Lemma 2.5
  • proof
  • Remark 2.6
  • Definition 3.1
  • ...and 55 more