ABSTRACT
This article re-examines Lawvere's abstract, category-theoretic proof of the fixed-point theorem whose contrapositive is a `universal' diagonal argument. The main result is that the necessary axioms for both the fixed-point theorem and the diagonal argument can be stripped back further, to a semantic analogue of a weak substructural logic lacking weakening or exchange.
► BibTeX data
► References
[1] Samson Abramsky. “No-cloning in categorical quantum mechanics”. In: Semantic techniques in quantum computation. https://doi.org/10.1017/CBO9781139193313.002, arXiv:0910.2401. Cambridge Univ. Press, Cambridge, 2010, pp. 1–28.
https://doi.org/10.1017/CBO9781139193313.002
arXiv:0910.2401
[2] Samson Abramsky and Jonathan Zvesper. “From Lawvere to Brandenburger-Keisler: Interactive Forms of Diagonalization and Self-reference”. In: Coalgebraic Methods in Computer Science. Ed. by Dirk Pattinson and Lutz Schröder. https://doi.org/10.1016/j.jcss.2014.12.001, arXiv:1006.0992. 2012, pp. 1–19.
https://doi.org/10.1016/j.jcss.2014.12.001
arXiv:1006.0992
[3] John Baez and Mike Stay. “Physics, topology, logic and computation: a Rosetta Stone”. In: New structures for physics. Vol. 813. Lecture Notes in Phys. https://doi.org/10.1007/978-3-642-12821-9, arXiv:0903.0340. Springer, Heidelberg, 2011, pp. 95–172.
https://doi.org/10.1007/978-3-642-12821-9
arXiv:0903.0340
[4] Carsten Butz. “Regular Categories and Regular Logic”. In: BRICS LS-98-2 (1998). https://www.brics.dk/LS/98/2/.
https://www.brics.dk/LS/98/2/
[5] Georg Cantor. “Ueber eine elementare Frage der Mannigfaltigkeitslehre”. In: Jahresber. Dtsch. Math.-Ver. 1 (1892), pp. 75–78.
[6] Karel Chvalovský and Rostislav Horčík. “Full Lambek calculus with contraction is undecidable”. In: J. Symb. Log. 81.2 (2016). https://doi.org/10.1017/jsl.2015.18, pp. 524–540.
https://doi.org/10.1017/jsl.2015.18
[7] Alexei Davydov. “Nuclei of categories with tensor products”. In: Theory and Applications of Categories 18 (2007). http://www.tac.mta.ca/tac/volumes/18/16/18-16abs.html, arXiv:0708.2761, pp. 440–472.
arXiv:0708.2761
http://www.tac.mta.ca/tac/volumes/18/16/18-16abs.html
[8] Valeria de Paiva. Dialectica Categories: the Relevant version. Talk at ICM2018 logic-satellite meeting, Niteroi, Brazil, August 2018, https://www.slideshare.net/valeria.depaiva/dialectica-categories-the-relevant-version-valeria-de-paiva, 2018.
https://www.slideshare.net/valeria.depaiva/dialectica-categories-the-relevant-version-valeria-de-paiva
[9] Valeria de Paiva. Relevant Dialectica Categories. MIT Category Theory Seminar talk, https://youtu.be/HnxUYb4FGzY. Aug. 2020.
https://youtu.be/HnxUYb4FGzY
[10] Kosta Došen and Zoran Petrić. “Relevant categories and partial functions”. In: Publications de l’Institut Mathématique 82 (2007). https://doi.org/10.2298/PIM0796017D, arXiv:math/0504133, pp. 17–23.
https://doi.org/10.2298/PIM0796017D
arXiv:math/0504133
[11] Martín Hötzel Escardó. On Lawvere’s Fixed Point Theorem (LFPT). Commented agda code available at https://www.cs.bham.ac.uk/ mhe/agda-new/LawvereFPT.html. 2018.
https://www.cs.bham.ac.uk/%20mhe/agda-new/LawvereFPT.html
[12] Robert Feys. “Les Logiques nouvelles des modalités”. In: Revue néoscolastique de philosophie 40 (1937). Available from https://www.jstor.org/stable/26346052, pp. 517–553.
https://www.jstor.org/stable/26346052
[13] Misha Gromov. Ergostuctures, Ergologic and the Universal Learning Problem: Chapters 1, 2. https://www.ihes.fr/ gromov/wp-content/uploads/2018/08/ergologic31.pdf. 2013.
https://www.ihes.fr/%20gromov/wp-content/uploads/2018/08/ergologic31.pdf
[14] Bart Jacobs. “Semantics of lambda-${\rm I}$ and of other substructure lambda calculi”. In: Typed lambda calculi and applications (Utrecht, 1993). Vol. 664. Lecture Notes in Comput. Sci. https://doi.org/10.1007/BFb0037107. Springer, Berlin, 1993, pp. 195–208.
https://doi.org/10.1007/BFb0037107
[15] F. William Lawvere. “Diagonal arguments and Cartesian closed categories”. In: Repr. Theory Appl. Categ. 15 (2006). Reprinted from Category Theory, Homology Theory and their Applications, II (Battelle Institute Conference, Seattle, Wash., 1968, Vol. Two) pp. 134–145, https://doi.org/10.1007/BFb0080769.
https://doi.org/10.1007/BFb0080769
[16] F. William Lawvere and Stephen H. Schanuel. Conceptual mathematics. 2nd Edition. https://doi.org/10.1017/CBO9780511804199. Cambridge University Press, Cambridge, 2009.
https://doi.org/10.1017/CBO9780511804199
[17] Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. “Internal universes in models of homotopy type theory”. In: rd International Conference on Formal Structures for Computation and Deduction. Vol. 108. LIPIcs. Leibniz Int. Proc. Inform. https://doi.org/10.4230/LIPIcs.FSCD.2018.22, arXiv:1801.07664. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2018, Art. No. 22, 17.
https://doi.org/10.4230/LIPIcs.FSCD.2018.22
arXiv:1801.07664
[18] William McCune and Larry Wos. “A case study in automated theorem proving: finding sages in combinatory logic”. In: J. Automat. Reasoning 3.1 (1987). https://doi.org/10.1007/BF00381147, pp. 91–107.
https://doi.org/10.1007/BF00381147
[19] María Claudia Meré. “Lógicas Relevantes: formalismo e semântica”. Available from https://www.dbd.puc-rio.br/deptoinformatica/93mere.pdf. PhD thesis. Pontifícia Universidade Católica do Rio de Janeiro, 1993.
https://www.dbd.puc-rio.br/deptoinformatica/93mere.pdf
[20] Robert K. Meyer. “Conservative extension in relevant implication”. In: Studia Logica 31 (1972). https://doi.org/10.1007/BF02120525, pp. 40–46.
https://doi.org/10.1007/BF02120525
[21] Robert K. Meyer and Richard Routley. “Algebraic analysis of entailment. I”. In: Logique et Anal. (N.S.) 15 (1972). https://www.jstor.org/stable/44083856, pp. 407–428. issn: 0024-5836.
https://www.jstor.org/stable/44083856
[22] Bartosz Milewski. How to get enriched over magmas and monoids. Blog post, https://bartoszmilewski.com/2014/09/29/how-to-get-enriched-over-magmas-and-monoids/. 2014.
https://bartoszmilewski.com/2014/09/29/how-to-get-enriched-over-magmas-and-monoids/
[23] Philip S. Mulry. “A categorical approach to the theory of computation”. In: Ann. Pure Appl. Logic 43.3 (1989). https://doi.org/10.1016/0168-0072(89)90072-9, pp. 293–305.
https://doi.org/10.1016/0168-0072(89)90072-9
[24] Peter W. O’Hearn, A. John Power, Makoto Takeyama, and Robert D. Tennent. “Syntactic control of interference revisited”. In: Mathematical foundations of programming semantics (New Orleans, LA, 1995). Vol. 1. Electron. Notes Theor. Comput. Sci. https://doi.org/10.1016/S1571-0661(04)00026-X. Elsevier Sci. B. V., Amsterdam, 1995, pp. 447–486.
https://doi.org/10.1016/S1571-0661(04)00026-X
[25] Hiroakira Ono. “Structural rules and a logical hierarchy”. In: Mathematical logic. https://doi.org/10.1007/978-1-4613-0609-2. Plenum, New York, 1990, pp. 95–104.
https://doi.org/10.1007/978-1-4613-0609-2
[26] Greg Restall. “Modalities in substructural logics”. In: Logique et Anal. (N.S.) 36.141-142 (1993). https://www.jstor.org/stable/44084365, pp. 25–38. issn: 0024-5836.
https://www.jstor.org/stable/44084365
[27] Greg Restall. An Introduction to Substructural Logics. Routledge, 2000.
[28] Dana S. Scott. “Relating theories of the $\lambda $-calculus”. In: To H. B. Curry: essays on combinatory logic, lambda calculus and formalism. Academic Press, London-New York, 1980, pp. 403–450.
[29] Peter Selinger. “Categorical structure of asynchrony”. In: MFPS XV: Mathematical Foundations of Programming Semantics, Fifteenth Conference (New Orleans, LA, 1999). Vol. 20. Electron. Notes Theor. Comput. Sci. https://doi.org/10.1016/S1571-0661(04)80073-2. Elsevier Sci. B. V., Amsterdam, 1999, 24 pp.
https://doi.org/10.1016/S1571-0661(04)80073-2
[30] Michael Shulman. “Brouwer’s fixed-point theorem in real-cohesive homotopy type theory”. In: Math. Structures Comput. Sci. 28.6 (2018). https://doi.org/10.1017/S0960129517000147, arXiv:1509.07584, pp. 856–941.
https://doi.org/10.1017/S0960129517000147
arXiv:1509.07584
[31] Raymond M. Smullyan. To Mock a Mocking Bird and Other Logic Puzzles: Including an Amazing Adventure in Combinatory Logic. Knopf, 1985.
[32] M. E. Szabo. Algebra of proofs. Vol. 88. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam-New York, 1978, pp. xii+297.
[33] Kornél Szlachányi. “Skew-monoidal categories and bialgebroids”. In: Advances in Mathematics 231.3 (2012). https://doi.org/10.1016/j.aim.2012.06.027, arXiv:1201.4981, pp. 1694–1730.
https://doi.org/10.1016/j.aim.2012.06.027
arXiv:1201.4981
[34] The Agda Team. Agda documentation: Flat Modality. https://agda.readthedocs.io/en/latest/language/flat.html. 2021.
https://agda.readthedocs.io/en/latest/language/flat.html
[35] Vladimir L. Vasyukov. “Paraconsistency in categories: case of relevance logic”. In: Studia Logica 98.3 (2011). https://doi.org/10.1007/s11225-011-9342-2, pp. 429–443.
https://doi.org/10.1007/s11225-011-9342-2
[36] David Walker. “Substructural Type Systems”. In: Advanced Topics in Types and Programming Languages. The MIT Press, 2005, pp. 3–43.
[37] Gijs Jasper Wijnholds. “Coherent diagrammatic reasoning in compositional distributional semantics”. In: Logic, language, information, and computation. Vol. 10388. Lecture Notes in Comput. Sci. https://doi.org/10.1007/978-3-662-55386-2. Springer, Berlin, 2017, pp. 371–386.
https://doi.org/10.1007/978-3-662-55386-2
[38] Georg H. von Wright. An essay in modal logic. Vol. 5. Studies in Logic and the Foundations of Mathematics. North-Holland, 1951.
[39] Noson S. Yanofsky. “A universal approach to self-referential paradoxes, incompleteness and fixed points”. In: Bull. Symbolic Logic 9.3 (2003). https://doi.org/10.2178/bsl/1058448677, arXiv:math/0305282, pp. 362–386.
https://doi.org/10.2178/bsl/1058448677
arXiv:math/0305282
Cited by
On Crossref's cited-by service no data on citing works was found (last attempt 2024-04-27 10:11:31). On SAO/NASA ADS no data on citing works was found (last attempt 2024-04-27 10:11:32).
This Paper is published in Compositionality under the Creative Commons Attribution 4.0 International (CC BY 4.0) license. Copyright remains with the original copyright holders such as the authors or their institutions.