Hostname: page-component-586b7cd67f-r5fsc Total loading time: 0 Render date: 2024-11-20T12:30:52.408Z Has data issue: false hasContentIssue false
  • English
  • Français

FIBRED ALGEBRAIC SEMANTICS FOR A VARIETY OF NON-CLASSICAL FIRST-ORDER LOGICS AND TOPOLOGICAL LOGICAL TRANSLATION

Part of: General logic Categories and theories Categories with structure Algebraic logic

Published online by Cambridge University Press:  10 June 2021

YOSHIHIRO MARUYAMA
YOSHIHIRO MARUYAMA*
Affiliation:
RESEARCH SCHOOL OF COMPUTER SCIENCE THE AUSTRALIAN NATIONAL UNIVERSITYCANBERRA, ACT, AUSTRALIAE-mail:yoshihiro.maruyama@anu.edu.au
Get access Rights & Permissions [Opens in a new window]

Abstract

Lawvere hyperdoctrines give categorical algebraic semantics for intuitionistic predicate logic. Here we extend the hyperdoctrinal semantics to a broad variety of substructural predicate logics over the Typed Full Lambek Calculus, verifying their completeness with respect to the extended hyperdoctrinal semantics. This yields uniform hyperdoctrinal completeness results for numerous logics such as different types of relevant predicate logics and beyond, which are new results on their own; i.e., we give uniform categorical semantics for a broad variety of non-classical predicate logics. And we introduce an analogue of Lawvere–Tierney topology and cotopology in the hyperdoctrinal setting, which gives a unifying perspective on different logical translations, in particular allowing for a uniform treatment of Girard’s exponential translation between linear and intuitionistic logics and of Kolmogorov’s double negation translation between intuitionistic and classical logics. In the hyerdoctrinal conception, type theories are categories, logics over type theories are functors, and logical translations between them, then, are natural transformations, in particular Lawvere–Tierney topologies and cotopologies on hyperdoctrines. The view of logical translations as hyperdoctrinal Lawvere–Tierney topologies and cotopologies has not been elucidated before, and may be seen as a novel contribution of the present work. From a broader perspective, this work may be regarded as taking first steps towards interplay between algebraic and categorical logics; it is, technically, a combination of substructural (or Lambekian) algebraic logic and hyperdoctrinal (or Lawverian) categorical logic, as the hyperdoctrinal completeness theorem is shown via the integration of the Lindenbaum–Tarski algebra construction with the syntactic category construction. As such this work lays a foundation for further interactions between algebraic and categorical logics.

Keywords

tripos theorytopos theoryhyperdoctrineLawvere-Tierney topologycategorical logicalgebraic logicsubstructural logic

MSC classification

Primary: 03G30: Categorical logic, topoi
Secondary: 18C10: Theories (e.g. algebraic theories), structure, and semantics 03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) 18D30: Fibered categories
Type
Article
Information
The Journal of Symbolic Logic , Volume 86 , Issue 3 , September 2021 , pp. 1189 - 1213
Check for updates
Copyright
© Association for Symbolic Logic 2021

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Adámek, J., Herrlich, H., and Strecker, G.E., Abstract and Concrete Categories, Wiley, Hoboken, 1990.Google Scholar
Ambler, S. J., First order linear logic in symmetric monoidal closed categories, Ph.D. thesis, University of Edinburgh, 1991.Google Scholar
Biering, B., Birkedal, L., and Torp-Smith, N., BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 29 (2007), no. 5, p. 24.CrossRefGoogle Scholar
Ciabattoni, A., Galatos, N., and Terui, K., Algebraic proof theory for substructural logics. Annals of Pure and Applied Logic, vol. 163 (2012), pp. 266–290.CrossRefGoogle Scholar
Ciabattoni, A., Galatos, N., and Terui, K., Algebraic proof theory: Hypersequents and hypercompletions. Annals of Pure and Applied Logic, vol. 168 (2017), pp. 693–737.CrossRefGoogle Scholar
Coumans, D., Canonical extensions in logic—some applications and a generalisation to categories, Ph.D. thesis, Radboud Universiteit Nijmegen, 2012.Google Scholar
Coumans, D., Gehrke, M., and van Rooijen, L., Relational semantics for full linear logic . The Journal of Applied Logics, vol. 12 (2014), pp. 50–66.CrossRefGoogle Scholar
Ferreira, G. and Oliva, P., On the relation between various negative translations, Logic, Construction, Computation (Berger, U., Diener, H., Schuster, P., and Seisenberger, M., editors), De Gruyter, Berlin, 2012, pp. 227–258.CrossRefGoogle Scholar
Frey, J., A 2-categorical analysis of the tripos-to-topos construction, preprint, 2011, arXiv:1104.2776.Google Scholar
Galatos, N., Jipsen, P., Kowalski, T., and Ono, H., Residuated Lattices: An Algebraic Glimpse at Substructural Logics , Elsevier, Amsterdam, 2007.Google Scholar
Galatos, N. and Ono, H., Glivenko theorems for substructural logics over FL. this Journal, vol. 71 (2016), pp. 1353–1384.Google Scholar
Henkin, L., Monk, J.D., and Tarski, A., Cylindric Algebras , North-Holland, Amsterdam, 1971.Google Scholar
Höhle, U. and Kubiak, T., A non-commutative and non-idempotent theory of quantale sets . Fuzzy Sets and Systems , vol. 166 (2011), pp. 1–43.CrossRefGoogle Scholar
Hyland, M., Johnstone, P.T., and Pitts, A., Tripos theory . Mathematical Proceedings of the Cambridge Philosophical Society , vol. 88 (1980), pp. 205–232.CrossRefGoogle Scholar
Hyland, M. and Power, J., The category theoretic understanding of universal algebra: Lawvere theories and monads . Electronic Notes in Theoretical Computer Science , vol. 172 (2007), pp. 437–458.CrossRefGoogle Scholar
Jacobs, B., Categorical Logic and Type Theory , Elsevier, Amsterdam, 1999.Google Scholar
Johnstone, P.T., Stone Spaces, Cambridge University Press, Cambridge, 1982.Google Scholar
Johnstone, P.T., Sketches of an Elephant, Oxford University Press, Oxford, 2002.Google Scholar
Kupke, C., Kurz, A., and Venema, Y., Stone coalgebras. Theoretical Computer Science, vol. 327 (2004), pp. 109–134.CrossRefGoogle Scholar
Lambek, J. and Rattray, B.A., A general Stone–Gelfand duality . Transactions of the American Mathematical Society, vol. 248 (1979), pp. 1–35.Google Scholar
Lambek, J. and Scott, P.J., Introduction to Higher-Order Categorical Logic , Cambridge University Press, Cambridge, 1986.Google Scholar
Lawvere, F.W., Functorial semantics of algebraic theories . Proceedings of the National Academy of Sciences of the United States of America , vol. 50 (1963), pp. 869–872.CrossRefGoogle ScholarPubMed
Lawvere, F.W., Adjointness in foundations. Dialectica, vol. 23 (1969), pp. 281–296.CrossRefGoogle Scholar
Marquis, J.-P. and Reyes, G., The history of categorical logic: 1963–1977, Handbook of the History of Logic (Gabbay, D. M., Kanamori, A., and Woods, J., editors), vol. 6, Elsevier, Amsterdam, 2011, pp. 689–800.Google Scholar
Maruyama, Y., Fundamental results for pointfree convex geometry . The Annals of Pure and Applied Logic , vol. 161 (2010), pp. 1486–1501.CrossRefGoogle Scholar
Maruyama, Y., Natural duality, modality, and coalgebra . Journal of Pure and Applied Algebra , vol. 216 (2012), pp. 565–580.CrossRefGoogle Scholar
Maruyama, Y., Categorical duality theory: With applications to domains, convexity, and the distribution monad . Leibniz International Proceedings in Informatics, CSL , vol. 23 (2013), pp. 500–520.Google Scholar
Maruyama, Y., Full lambek hyperdoctrine: Categorical semantics for first-order substructural logics , International Workshop on Logic, Language, Information, and Computation (WoLLIC) (Libkin, L., Kohlenbach, U., and de Queiroz, R., editors), Lecture Notes in Computer Science, vol. 8071, Springer, Heidelberg, 2013, pp. 211–225.CrossRefGoogle Scholar
Maruyama, Y., Duality theory and categorical universal logic: With emphasis on quantum structures. Proceedings of the 10th Quantum Physics and Logic Conference, EPTCS (B. Coecke and M. J. Hoban, editors), Barcelona, 2014, pp. 100–112.CrossRefGoogle Scholar
Maruyama, Y., Topological duality via maximal spectrum functor. Communications in Algebra, vol. 48 (2020), pp. 2616–2623.CrossRefGoogle Scholar
Maruyama, Y., First-order typed fuzzy logics and their categorical semantics: Linear completeness and Baaz translation via Lawvere hyperdoctrine theory, Proceedings of FUZZ-IEEE (Cordon, O., Hagras, H., Lam, H. K., and Lin, C. T., editors), IEEE Computational Intelligence Society Press, 2020, pp. 1–8.Google Scholar
Maruyama, Y., Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory , Lecture Notes in Computer Scienc, vol. 12062, Springer, Berlin, 2020, pp. 187–203.Google Scholar
Ono, H., Algebraic semantics for predicate logics and their completeness . RIMS Kokyuroku , vol. 927 (1995), pp. 88–103.Google Scholar
Ono, H., Crawley completions of residuated lattices and algebraic completeness of substructural predicate logics . Studia Logica , vol. 100 (2012), pp. 339–359.CrossRefGoogle Scholar
Pitts, A., Categorical logic , Handbook of Logic in Computer Science (Abramsky, S., Gabbay, D. M., and Maibaum, T. S. E., editors), vol. 5, Oxford University Press, Oxford, 2000, pp. 39–123.Google Scholar
Pitts, A., Tripos theory in retrospect . Mathematical Structures in Computer Science , vol. 12 (2002), pp. 265–279.CrossRefGoogle Scholar
Seely, R.A.G., Linear logic, *-autonomous categories and cofree coalgebras, Categories in Computer Science and Logic (Gray, J. W. and Scedrov, A., editors), American Mathematical Society, Providence, 1989, pp. 371–382.CrossRefGoogle Scholar
White, R.B., The consistency of the axiom of comprehension in the infinite-valued predicate logic of Łukasiewicz. Journal of Philosophical Logic, vol. 8 (1979), pp. 509–534.CrossRefGoogle Scholar