Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory

Higher-order intuitionistic logic categorically corresponds to toposes or triposes; here we address what are toposes or triposes for higher-order substructural logics. Full Lambek calculus gives a framework to uniformly represent different logical systems as extensions of it. Here we define higher-order Full Lambek calculus, which boils down to higher-order intuitionistic logic when equipped with all the structural rules, and give categorical semantics for (any extension of) it in terms of triposes or higher-order Lawvere hyperdoctrines, which were originally conceived for intuitionistic logic, and yet are flexible enough to be adapted for substructural logics. Relativising the completeness result thus obtained to different axioms, we can obtain tripos-theoretical completeness theorems for a broad variety of higher-order logics. The framework thus developed, moreover, allows us to obtain tripos-theoretical Girard and Kolmogorov translation theorems for higher-order logics.