Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-22T03:00:08.036Z Has data issue: false hasContentIssue false
  • English
  • Français

AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS

Part of: Proof theory and constructive mathematics

Published online by Cambridge University Press:  21 July 2022

MICHAEL SHULMAN
MICHAEL SHULMAN*
Affiliation:
DEPARTMENT OF MATHEMATICS UNIVERSITY OF SAN DIEGOSAN DIEGO, CA92110, USAE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We show that numerous distinctive concepts of constructive mathematics arise automatically from an “antithesis” translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically “constructivize” classical definitions, handling the resulting bookkeeping automatically.

Keywords

linear logicaffine logicconstructive mathematics

MSC classification

Primary: 03F52: Linear logic and other substructural logics
Secondary: 03F65: Other constructive mathematics
Type
Articles
Information
Bulletin of Symbolic Logic , Volume 28 , Issue 3 , September 2022 , pp. 327 - 386
Check for updates
Copyright
© The Author(s), 2022. Published by Cambridge University Press on behalf of The Association for Symbolic Logic

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

Abramsky, S. and Lenisa, M., Linear realizability and full completeness for typed lambda-calculi . Annals of Pure and Applied Logic , vol. 134 (2005), no. 2, pp. 122–168.CrossRefGoogle Scholar
Abramsky, S., Haghverdi, E., and Scott, P., Geometry of interaction and linear combinatory algebras . Mathematical Structures in Computer Science , vol. 12 (2002), no. 5, pp. 625–665.CrossRefGoogle Scholar
Aczel, P. and Gambino, N., Collection principles in dependent type theory , Types for Proofs and Programs (P. Callaghan, Z. Luo, J. McKinna, and R. Pollack, editors), Springer, Berlin, 2002, pp. 1–23.Google Scholar
Awodey, S. and Kishida, K., Topology and modality: The topological interpretation of first-order modal logic . The Review of Symbolic Logic , vol. 1 (2008), no. 2, pp. 146–166.CrossRefGoogle Scholar
Awodey, S., Kishida, K., and Kotzsch, H.-C., Topos semantics for higher-order modal logic . Logique et Analyse , vol. 57 (2014), no. 228, pp. 591–636.Google Scholar
Barr, M., *-Autonomous Categories, Lecture Notes in Mathematics, vol. 752, Springer, Berlin, 1979.CrossRefGoogle Scholar
Barr, M., $\ast$ -autonomous categories and linear logic . Mathematical Structures in Computer Science , vol. 1 (1991), no. 2, pp. 159–178.CrossRefGoogle Scholar
Bartels, T. and Trimble, T., Cheng space, 2012. Available at https://ncatlab.org/nlab/show/Cheng+space.Google Scholar
Bishop, E., Foundations of Constructive Analysis, McGraw-Hill Series in Higher Mathematics, McGraw-Hill, New York, 1967.Google Scholar
Bishop, E. and Bridges, D., Constructive Analysis , Springer, Heidelberg, 1985.CrossRefGoogle Scholar
Bridges, D. S. and Vîţă, L. S., Apartness and Uniformity: A Constructive Development, Springer, Berlin–Heidelberg, 2011.CrossRefGoogle Scholar
Carboni, A., Lack, S., and Walters, R. F. C., Introduction to extensive and distributive categories . Journal of Pure and Applied Algebra, vol. 84 (1993), no. 2, pp. 145–158.CrossRefGoogle Scholar
Chu, P.-H., Constructing *- autonomous categories, M.Sc. thesis, McGill University, 1978.Google Scholar
Chu, P.-H., Constructing *-autonomous categories , *-Autonomous Categories, Lecture Notes in Mathematics, vol. 752, Springer, Berlin, 1979, Chapter Appendix.Google Scholar
Cockett, J. R. B. and Seely, R. A. G., Proof theory for full intuitionistic linear logic, bilinear logic, and MIX categories. Theory and Applications of Categories, vol. 3 (1997), no. 5, pp. 85–131.Google Scholar
Conway, J. H., On Numbers and Games, second ed., A K Peters, Natick, 2001.Google Scholar
Escardó, M. and Xu, C., The inconsistency of a Brouwerian continuity principle with the Curry–Howard interpretation, 13th International Conference on Typed Lambda Calculi and Applications (T. Altenkirch, editor), Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, 2015, pp. 153–164.Google Scholar
Forsberg, F. N. and Setzer, A., A finite axiomatisation of inductive-inductive definitions, Logic, Construction, Computation (U. Berger, H. Diener, P. Schuster, and M. Seisenberger, editors), De Gruyter, Berlin, 2013, pp. 259–288.Google Scholar
Girard, J.-Y., Linear logic . Theoretical Computer Science , vol. 50 (1987), no. 1, pp. 1–101.CrossRefGoogle Scholar
Gödel, K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes . Dialectica , vol. 12 (1958), pages 280–287.CrossRefGoogle Scholar
Grišin, V. N., Predicate and set-theoretic calculi based on logic without contractions . Mathematics of the USSR-Izvestiya , vol. 18 (1982), no. 1, pp. 41–59.CrossRefGoogle Scholar
Hofmann, M., On the interpretation of type theory in locally Cartesian closed categories, Proceedings of Computer Science Logic (L. Pacholski and J. Tiuryn, editors), Lecture Notes in Computer Science, Springer, Berlin, 1994, pp. 427–441.Google Scholar
Hofstra, P., The Dialectica monad and its cousins, Models, Logics, and Higher-Dimensional Categories: A Tribute to the Work of Mihály Makkai (B. Hart, T. G. Kucera, A. Pillay, P. J. Scott, and R. A. G. Seely, editors), American Mathematical Society, 2011, pp. 107–137.CrossRefGoogle Scholar
Hyland, J. M. E., Johnstone, P. T., and Pitts, A. M., Tripos theory . Mathematical Proceedings of the Cambridge Philosophical Society , vol. 88 (1980), no. 2, pp. 205–231.CrossRefGoogle Scholar
Jacobs, B., Categorical Logic and Type Theory , Studies in Logic and the Foundations of Mathematics, vol. 141, North-Holland, Amsterdam, 1999.Google Scholar
Johnstone, P. T., Rings, fields, and spectra. Journal of Algebra, vol. 49 (1977), no. 1, pp. 238–260.CrossRefGoogle Scholar
Johnstone, P. T., Sketches of an Elephant: A Topos Theory Compendium, vol. 2 , Oxford Logic Guides, 43, Oxford Science Publications, Oxford, 2002.Google Scholar
Lawvere, F. W., Equality in hyperdoctrines and comprehension schema as an adjoint functor , Applications of Categorical Algebra, American Mathematical Society, Providence, 1970, pp. 1–14.Google Scholar
Lawvere, F. W., Adjointness in foundations. Reprints in Theory and Applications of Categories, vol. 16 (2006), pp. 1–16 (electronic). Reprinted from Dialectica, vol. 23 (1969).Google Scholar
Lovas, W. and Crary, K., Structural normalization for classical natural deduction, 2006. Available at https://www.cs.cmu.edu/~wlovas/papers/clnorm.pdf.Google Scholar
Lumsdaine, P. L. and Warren, M. A., The local universes model: An overlooked coherence construction for dependent type theories . ACM Transactions on Computational Logic , vol. 16 (2015), no. 3, pp. 23:1–23:31.CrossRefGoogle Scholar
Makkai, M., Avoiding the axiom of choice in general category theory . Journal of Pure and Applied Algebra , vol. 108 (1996), no. 2, 109–173.CrossRefGoogle Scholar
McKinna, J., Deliverables: A categorical approach to program development in type theory, Ph.D. thesis, University of Edinburgh, 1992.CrossRefGoogle Scholar
Melliès, P.-A., Categorical semantics of linear logic , Interactive Models of Computation and Program Behaviour (P.-L. Curien, H. Herbelin, J.-L. Krivine, and P.-A. Melliès, editors), Panoramas et Synthèses, vol. 27, Société Mathématique de France, Paris, 2009, pp. 1–196.Google Scholar
Mines, R., Richman, F., and Ruitenburg, W., A Course in Constructive Algebra, Springer, Berlin, 1988.CrossRefGoogle Scholar
Nelson, D., Constructible falsity . The Journal of Symbolic Logic , vol. 14 (1949), no. 1, pp. 16–26.CrossRefGoogle Scholar
O’Hearn, P. W. and Pym, D. J., The logic of bunched implications, this Journal, vol. 5 (1999), no. 2, pp. 215–244.Google Scholar
Oliva, P., An analysis of Gödel’s Dialectica interpretation via linear logic . Dialectica , vol. 62 (2008), no. 2, pp. 269–290.CrossRefGoogle Scholar
de Paiva, V., The Dialectica categories, Categories in Computer Science and Logic (J. Gray and A. Scedrov, editors), Contemporary Mathematics, vol. 92, American Mathematical Society, Providence, 1989.Google Scholar
de Paiva, V., A Dialectica-like model of linear logic , Category Theory and Computer Science (D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, and A. Poigné, editors), Springer, Berlin–Heidelberg, 1989, pp. 341–356.CrossRefGoogle Scholar
de Paiva, V., Dialectica and Chu constructions: Cousins? Theory and Applications of Categories , vol. 17 (2006), no. 7, pp. 127–152.Google Scholar
Patterson, A. L., Implicit programming and the logic of constructible duality, Ph.D. thesis, University of Illinois at Urbana-Champaign, 1998.Google Scholar
Richman, F., Generalized real numbers in constructive mathematics . Indagationes Mathematicae , vol. 9 (1998), no. 4, pp. 595–606.CrossRefGoogle Scholar
Seely, R., Linear logic, *-autonomous categories and cofree coalgebras, Categories in Logic and Computer Science (J. W. Gray and A. Scedrov, editors), Contemporary Mathematics, vol. 92, American Mathematical Society, Providence, 1989.Google Scholar
Shramko, Y., Dual intuitionistic logic and a variety of negations: The logic of scientific research . Studia Logica , vol. 80 (2005), pp. 347–367.CrossRefGoogle Scholar
Shulman, M., The 2-Chu–Dialectica construction and the polycategory of multivariable adjunctions . Theory and Applications of Categories , vol. 35 (2020), no. 4, pp. 89–136.Google Scholar
Taylor, P., Intuitionistic sets and ordinals . The Journal of Symbolic Logic , vol. 61 (1996), no. 3, pp. 705–744.CrossRefGoogle Scholar
Trafford, J., Co-constructive logics for proofs and refutations . Studia Humana , vol. 3 (2015), no. 4, 22–40.CrossRefGoogle Scholar
Troelstra, A. S. and van Dalen, D., Constructivism in Mathematics , vol. I , Studies in Logic and the Foundations of Mathematics, vol. 121, North-Holland, Amsterdam, 1988.Google Scholar
Troelstra, A. S. and van Dalen, D., Constructivism in Mathematics , vol. II , Studies in Logic and the Foundations of Mathematics, vol. 123, North-Holland, Amsterdam, 1988.Google Scholar
Trotta, D., An algebraic approach to the completions of elementary doctrines, preprint, 2021, arXiv:2108.03415.Google Scholar
Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, first ed., 2013. Available at http://homotopytypetheory.org/book/.Google Scholar
Vickers, S., Topology via Logic , Cambridge Tracts in Theoretical Computer Science, vol. 5, Cambridge University Press, Cambridge, 1996.Google Scholar