A Monadic Second-Order Version of Tarski’s Geometry of Solids

Patrick Barlatier; Richard Dapoigny

doi:10.12775/LLP.2023.019

Authors

Patrick Barlatier LISTIC Polytech’Annecy-Chambéry, University Savoie Mont-Blanc
Richard Dapoigny LISTIC Polytech'Annecy-Chambéry, University Savoie Mont-Blanc

DOI:

https://doi.org/10.12775/LLP.2023.019

Keywords

mereology, monadic second-order logic, geometry of solids, calculus of inductive constructions, theorem prover, type theory

Abstract

In this paper, we are concerned with the development of a general set theory using the single axiom version of Leśniewski’s mereology. The specification of mereology, and further of Tarski’s geometry of solids will rely on the Calculus of Inductive Constructions (CIC). In the first part, we provide a specification of Leśniewski’s mereology as a model for an atomless Boolean algebra using Clay’s ideas. In the second part, we interpret Leśniewski’s mereology in monadic second-order logic using names and develop a full version of mereology referred to as CIC-based Monadic Mereology (λ-MM) allowing an expressive theory while involving only two axioms. In the third part, we propose a modeling of Tarski’s solid geometry relying on λ-MM. It is intended to serve as a basis for spatial reasoning. All parts have been proved using a translation in type theory.

References

Bennett, B., 2001, “A categorical axiomatisation of region-based geometry”, Fundamenta Informaticae, 46 (1–2): 145–158.

Bertot, Y., and P. Castéran, 2004, Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, An EATCS series, Springer Verlag.

Betti, A. and I. Loeb, 2012, “On Tarski’s foundations of the geometry of solids”, The Bulletin of Symbolic Logic, 18 (2): 230–260. DOI: http://dx.doi.org/10.2178/bsl/1333560806

Borgo, S., N. Guarino and C. Masolo, 1996, “A pointless theory of space based on strong connection and congruence”, pages 220–229 in L. Carlucci Aiello et al. (eds.), Procs. of the International Conference on Principles of Knowledge Representation and Reasoning (KR 1996), Morgan Kaufmann.

Borgo, S., and C. Masolo, 2010, “Full mereogeometries”, Review of Symbolic Logic, 3 (4): 521–567. DOI: http://dx.doi.org/10.1017/S1755020310000110

Casati, R., and A. C. Varzi, 1999, Parts and Places: The Structures of Spatial Representation, Cambridge (Ma): MIT Press.

Church, A., 1940, “A formulation of the simple theory of types”, Journal of Symbolic Logic, 5: 56–68.

Clay, R. E., 1969, “Sole axioms for partially ordered sets”, Logique et Analyse, 12 (48): 361–375.

Clay, R. E., 1974, “Relation of Leśniewski’s mereology to Boolean algebra”, The Journal of Symbolic Logic, 39 (4): 638–648. DOI: http://dx.doi.org/10.2307/2272847

Clay, R. E., 2021, “Leśniewski, Tarski and the geometry of solids”, Logique et Analyse, 254: 131–148. DOI: http://dx.doi.org/10.2143/LEA.254.0.3289654

Cocchiarella, N. B., 2001, “A conceptualist interpretation of Leśniewski’s ontology”, History and Philosophy of Logic, 22 (1): 29–43. DOI: http://dx.doi.org/10.1080/01445340110113381

Cotnoir, A. J. and A. Bacon, 2012, “Non-wellfounded mereology”, Review of Symbolic Logic, 5 (2): 187–204. DOI: http://dx.doi.org/10.1017/S1755020311000293

Cotnoir, A. J., 2021, “Is weak supplementation analytic?”, Synthese, 198 (18–S): 4229–4245. DOI: http://dx.doi.org/10.1007/s11229-018-02066-9

Czajka, Ł., and C. Kaliszyk, 2018, “Hammer for Coq: Automation for dependent type theory”, Journal of Automated Reasoning, 61, 423–453. DOI: http://dx.doi.org/10.1007/s10817-018-9458-4

Dapoigny, R., and P. Barlatier, 2015, “A Coq-based axiomatization of Tarski’s mereogeometry”, pages 108–129 in S. Fabrikant et al. (eds,), Spatial Information Theory, COSIT 2015, vol. 9368 of Lecture Notes in Computer Science, Springer. DOI: http://dx.doi.org/10.1007/978-3-319-23374-1 6

Dugat, V., P. Gambarotto and Y. Larvor, 1999, “Qualitative theory of shape and orientation”, pages 45–53 in R. V. Rodriguez (ed.), Procs. of the Workshop on Hot Topics in Spatial and Temporal Reasoning, International Joint Conference on Artificial Intelligence (IJCAI 1999).

Gruszczyński, R., and A. Pietruszczak, 2008, “Full development of Tarski’s geometry of solids”, Bulletin of Symbolic Logic, 14 (4): 481–540. DOI: http://dx.doi.org/10.2178/bsl/1231081462

Gruszczyński, R., and A. Pietruszczak, 2009, “Space, points and mereology. On foundations of point-free Euclidean geometry”, Logic and Logical Philosophy, 18 (2): 145–188. DOI: http://dx.doi.org/10.12775/LLP.2009.009

Hamkins, J. D., and M. Kikuchi, 2016, “Set-theoretic mereology”, Logic and Logical Philosophy, 25 (3): 285–308. DOI: http://dx.doi.org/10.12775/LLP.2016.007

Henkin, L., 1963, “A theory of propositional types”, Fundamenta Mathematicae, 52: 323–334.

Jaśkowski, S., 1948, “Une modification des définitions fondamentales de la géométrie des corps de M. A. Tarski”, Annales de la Société Polonaise de Mathématique, 21, 298–301.

Kaminski, M. and G. Smolka, 2008, “A minimal propositional type theory”, Technical Report, Saarland University.

Lejewski, C., 1963, “A note on a problem concerning the axiomatic foundations of mereology”, Notre Dame Journal of Formal Logic, 4 (2): 135–139. DOI: http://dx.doi.org/10.1305/ndjfl/1093957503

Lejewski, C., 1967, “A single axiom for the mereological notion of proper part”, Notre Dame Journal of Formal Logic, 8 (4): 279–285. DOI: http://dx.doi.org/10.1305/ndjfl/1094068839

Leonard, H. S., and N. Goodman, 1940, “The calculus of individuals and its uses”, The Journal of Symbolic Logic, 5 (2): 45–55.

Leśniewski, S., 1916, “Podstawy ogólnej teoryi mnogosci.”, Moskow: Prace Polskiego Kola Naukowego w Moskwie, Sekcya matematyczno-przyrodnicza, (English translation 1992, by D. I. Barnett: “Foundations of the general theory of sets. I”, pages 129–173 in S. Leśniewski, Collected Works, S. J. Surma, J. Srzednicki, D. I. Barnett, and F. V. Rickey (eds.), volume 44 of Nijhoff nternational Philosophy Series, Dordrecht: Kluwer, 1992.

Lewis, D., 1991, Parts of Classes, Blackwell. DOI: http://dx.doi.org/10.2307/2219902

Makowsky, J. A., 2004, “Algorithmic uses of the Feferman-Vaught theorem”, Annals of Pure and Applied Logic, 126 (1–3): 159–213. DOI: http://dx.doi.org/10.1016/j.apal.2003.11.002

Pietruszczak, A., 1996, “Mereological sets of distributive classes”, Logic and Logical Philosophy, 4: 105–122. DOI: http://dx.doi.org/10.12775/LLP.1996.005

Pietruszczak, A., 2005, “Pieces of mereology”, Logic and Logical Philosophy, 14 (2): 211–234. DOI: http://dx.doi.org/10.12775/LLP.2005.014

Pietruszczak, A., 2015, “Classical mereology is not elementarily axiomatizable”, Logic and Logical Philosophy, 24 (4): 485–498. DOI: http://dx.doi.org/10.12775/LLP.2015.017

Pietruszczak, A., 2020, Foundations of the Theory of Parthood. A Study of Mereology, Trends in Logic, vol. 54, Springer International Publishing. DOI: http://dx.doi.org/10.1007/978-3-030-36533-2

Simons, P., 1987, Parts: A Study in Ontology, Second Edition, Clarendon Press, Oxford. DOI: http://dx.doi.org/10.1093/acprof:oso/9780199241460.001.0001

Sinisi, V. F., 1983, “Leśniewski’s foundations of mathematics”, Topoi, 2:3–52. DOI: http://dx.doi.org/10.1007/BF00139700

Smirnov, V. A., 1987, “Strict embedding of the elementary ontology into the monadic second-order calculus of predicates admitting the empty individual domain”, Studia Logica, 46 (1): 1–15. DOI: http://dx.doi.org/10.1007/BF00396902

Sobociński, B., 1984, “Studies in Leśniewski’s mereology”, pages 217–227 in V. F. Rickey, J. T. Srzednicki (eds.), Leśniewski’s Systems: Ontology and Mereology, vol. 13 of Nijhoff International Philosophy Series, Martinus Nijhoff Publishers, Kluwer Academic Publishers Group. DOI: http://dx.doi.org/10.1007/978-94-009-6089-3

Tarski, A., 1929, “Les fondements de la géométrie des corps”, pages 29–33 in Annales de la société Polonaise de Mathématiques, Kraków.

Tarski, A., 1956a, “Fundations of the geometry of solids”, pages 24–29 in Logic, Semantics, Metamathematics: Papers from 1923 to 1938, J. H. Woodger (ed.), Clarendon Press: Oxford.

Tarski, A., 1956b, “On the foundation of Boolean algebra”, pages 320–341 in Logic, Semantics, Metamathematics: Papers from 1923 to 1938, J. H. Woodger (ed.), Clarendon Press: Oxford.

Tsai, H., 2013, “A comprehensive picture of the decidability of mereological theories”, Studia Logica, 101(5): 987–1012. DOI: http://dx.doi.org/10.1007/s11225-012-9405-z

Tsai, H., 2015, “Notes on models of first-order mereological theories”, Logic and Logical Philosophy, 24 (4): 469–482. DOI: http://dx.doi.org/10.12775/LLP.2015.009

Varzi, A. C., 1996, “Parts, wholes, and part-whole relations: The prospects of mereotopology”, Data and Knowledge Engineering, 20 (3): 259–286. DOI: 1 http://dx.doi.org/0.1016/S0169-023X(96)00017-1

Welch, P. D., and L. F. M. Horsten, 2016, “Reflecting on absolute infinity”, Journal of Philosophy, 113 (2): 89–111. DOI: http://dx.doi.org/10.5840/jphil201611325

Wenzel, M., L. C. Paulson and T. Nipkow, 2008, “The Isabelle Framework”, pages 33–38 in Procs. of Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada. DOI: http://dx.doi.org/10.1007/978-3-540-71067-7_7