Coherence in Cartesian closed categories and the generality of proofs (Q750442)

Following to program of establishing fundamental correspondence between logic and category theory originated by J. Lambek, the author considers the problem of distinguishing arrows of free Cartesian closed category presented by corresponding intuitionistic propositional cut-free proofs. This is done in terms of a notion of generality of proofs and is based on deductive considerations, in contrast to formerly considered functorial generality notion. Any given proof f: \(\Gamma\to A\) is first ``expanded to a congruent proof \(f^*: \Gamma \to A\) which does not contain citation of axioms that are equivalent to thinnings and in which applications of the rule (\(\Rightarrow\to)\) precede applications of the rule (\(\to \&)\) whenever syntactically possible''. Then rename in \(\Gamma\to A\) each occurrence of a propositional variable in order from left to right by a distinct letter and rewrite the proof \(f^*: \Gamma \to A\) by renaming all ancestors of a variable with their new names. Finally, generality of a given proof f: \(\Gamma\to A\) is defined as the pair \(\alpha\mapsto \beta\), where \(\alpha\) and \(\beta\) are sequences of new names of occurrences of propositional variables from left to right in \(\Gamma\to A\) and, resp., in axioms of the expanded proof \(f^*: \Gamma \to A\). (Axioms are sequents \(X\to X\) with X propositional variable). Theorem (Coherence). Two cut-free proofs f and g of a sequent \(\Gamma\to A\) represent the same arrow in the free Cartesian closed category iff f and g have the same generality. No explicit proof of this is presented, but there are numerous illustrative examples.