McGill University Thèses et mémoires par auteur commençant par Č

We prove a completeness result for the equivalence of proofs in the positive fragment (T, $ Lambda, rightarrow$) of intuitionistic propositional logic with respect to sets. We also show that proofs in the full intuitionistic propositional logic factor through interpolants--in this way we prove a stronger interpolation property than the usual one which gives only the existence of interpolants. Translating that to categorical terms, we give a representation theroem for free Cartesian closed categories (Theorem 3.16) in the category of sets and we show that pushouts of biCartesian closed categories have the interpolation property (Theorem 4.47).  Lire la suite