TY - GEN
T1 - Higher-Order Categorical Substructural Logic
T2 - 18th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2020
AU - Maruyama, Yoshihiro
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85083983160&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-43520-2_12
DO - 10.1007/978-3-030-43520-2_12
M3 - Conference contribution
AN - SCOPUS:85083983160
SN - 9783030435196
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 187
EP - 203
BT - Relational and Algebraic Methods in Computer Science - 18th International Conference, RAMiCS 2020, Proceedings
A2 - Fahrenberg, Uli
A2 - Jipsen, Peter
A2 - Winter, Michael
PB - Springer
Y2 - 8 April 2020 through 11 April 2020
ER -