Till Mossakowski, Joseph Goguen: An Institutional View on the Curry-Howard-Tait-Isomorphism
The well-known Curry-Howard-Tait isomorphism establishes a
correspondence between
- propositions and types
- proofs and terms
- proof reductions and term reductions
Moreover, in this context, a number of deep correspondences
between categories and logical theories have been established:
- propositional logic with conjunction corresponds to cartesian categories
-
- propositional logic with conjunction and implication corresponds cartesian closed categories
- intuitionistic propositional logic corresponds to bicartesian closed categories
- classical propositional logic corresponds to bicartesian closed categories with not not-elimination
- first-order logic corresponds hyperdoctrines
- Martin-Löf type theory corresponds to locally cartesian closed categories
Can this isomorphism be presented in an institutional setting,
as a relation between institutions?
We answer this question positively for the propositional case,
and give a general notion of propositional categorical logic,
a construction of an institution with proofs out of such a logic,
and a logic-independent soundness and completeness theorem.
While all this is clearly limited to propositional logics,
we conclude with some speculations how to extend this program
to other logics.