The “ontological square” and modern type theories


V. V. Dolgorukov
A. O. Kopylova


This paper focuses on the connection between “four-category ontologies” (which are based on Aristotle's ontological square) and modern type-theoretical semantics.
Four-category ontologies make a distinction between four types of entities: substantial universals, substantial particulars, accidental universals and accidental particulars.
According to B. Smith, “fantology is a doctrine to the effect that the key to the ontological structure of reality is captured syntactically in the 'Fa' ”.

Smith argues that predicate logic cannot adequately describe these four types of entities, which are reduced to just two kinds the general ('$F$') and the particular ('$a$').
B. Smith has criticized G. Frege's predicate logic. He argues that Frege, being the father of modern logic, simultaneously became the father of “fantology” with its ontological commitments.

Smith transforms the ontological square to the ontological sextet (which also involves universal and particular events) and proposes a set of predicates for different ontological relations connecting these six types of entities.

However, Smith's approach has a number of limitations: he suggests a theory that describes only predicates of different types as universals. We argue for another formalization for the ontological square's entities. This approach is based on modern type-theoretical semantics, according to which, the difference between substantial universals and accidental universals can be expressed. In first-order logic the sentences “Socrates is a man” and “Socrates is wise” share the same logical form. However, this fact is not consistent with “ontological square” metaphysics (“being a man” is a substantial universal and “being wise” is an accidental universal). Whereas, according to the type-theoretical approach, relations to accidental universals are expressed by judgments about type ($a\!:A$), but relations to accidental universals are expressed by predication ('$a$'). DOI: 10.21146/2074-1472-2018-24-2-36-58






Аристотель. Категории // Аристотель. Соч.: в 4 т. Т. 2. М.: Мысль, 1978. 687 c.
Angelelli I. Studies on Gottlob Frege and Traditional Philosophy. Dordrecht: Reidel, 1967. 291 p.
Asher N. Lexical Meaning in Context: a Web of Words. Cambridge: Cambridge University Press, 2012. 346 p.
Back A. Aristotle’s Theory of Predication. Leiden: Brill, 2000. 348 p.
Bekki D. Representing Anaphora with Dependent Types // Logical Aspects of Computational Linguistics / Eds. by N. Asher, S. Soloviev. Heidelberg: Springer, 2014. P. 14–29.
Boldini P. Formalizing Context in Intuitionistic Type Theory // Fundamenta Informaticae. 2000. Vol. 42. No. 2. P. 1–23.
Campbell K. The Metaphysic of Abstract Particulars // Midwest Studies In Philosophy. 1981. Vol. 1. No. 6. P. 477–488.
Campbell K. Abstract Particulars. Oxford: Blackwell, 1990. 220 p.
Chatzikyriakidis S., Luo Z. Natural Language Inference in Coq // Journal of Logic, Language and Information. 2014. Vol. 4. No. 23. P. 441–480.
Chatzikyriakidis S., Luo Z. Adjectival and Adverbial Modification: The View from Modern Type Theories // Journal of Logic, Language and Information. 2017. Vol. 1. No. 26. P. 45–88.
Chatzikyriakidis S., Luo Z. (eds.) Modern Perspectives in Type-Theoretical Semantics. Dordrecht: Springer, 2017. 296 p.
Church A. A Formulation of the Simple Theory of Types // The Journal of Symbolic Logic. 1940. Vol. 5. No. 1. P. 56–68.
Cooper R. Records and Record Types in Semantic Theory // Journal of Logic and Computation. 2005. Vol. 15. No. 2. P. 99–112.
Denkel A. Object and Property. Cambridge: Cambridge University Press, 1996. 276 p.
Francez N., Dyckhoff R. Proof-Theoretic Semantics for a Natural Language Fragment // Linguistics and Philosophy. 2010. Vol. 33. No. 6. P. 447–477.
Geach P. Reference and Generality: An Examination of Some Medieval and Modern Theories. Ithaca: Cornell University Press, 1962. 202 p.
Granstrom J.G. Treatise on Intuitionistic Type Theory. Dordrecht: Springer, 2011. 196 p.
Loux M. Substance and Attribute. Dordrecht: Reidel, 1978. 188 p.
Lowe E.J. The Possibility of Metaphysics. Substance, Identity, and Time. Oxford: Clarendon Press, 1998. 288 p.
Lowe E.J. The Four-Category Ontology. A Metaphysical Foundation for Natural Science. Oxford: Oxford University Press, 2006. 222 p.
Lowe E.J. Forms of Thought: A Study in Philosophical Logic. Cambridge: Cambridge University Press, 2013. 226 p.
Luo Z. Computation and Reasoning: A Type Theory for Computer Science. Oxford: Oxford University Press, 1994. 240 p.
Luo Z. Coercive Subtyping // Journal of Logic and Computation. 1999. Vol. 9. No. 1. P. 105–130.
Luo Z. Formal Semantics in Modern Type Theories with Coercive Subtyping // Linguistics and Philosophy. 2012. Vol. 35. No. 6. P. 491–513.
Martin-Lof P. Intuitionistic Type Theory. Napoli: Bibliopolis, 1984. 91 p.
McMahon W.E. Strawson and the Aristotelian Ontological Square // Studies in Language. 1977. Vol. 3. No. 1. P. 363–378.
Moltmann F. Nominalizing quantifiers // Journal of Philosophical Logic. 2003. Vol. 32. No. 5. P. 445–481.
Moltmann F. Two Kinds of Universals and Two Kinds of Collections // Linguistics and Philosophy. 2005. Vol. 6. No. 27. P. 739–776.
Montague R. The Proper Treatment of Quantification in Ordinary English // Approaches to natural language. Proceedings of the 1970 Stanford workshop on grammar and semantics / Eds. J. Hintikka, J. Moravcsik, P. Suppes. Dordrecht: Reidel, 1973.
Montague R. Formal philosophy. New Haven: Yale University Press, 1974. 370 p.
Neuhaus F., Grenon P., Smith B. A Formal Theory of Substances, Qualities, and Universals // Formal Ontology in Information Systems. Proceedings of the Third International Conference / Eds. by A. Varzi, L. Vieu. IOS Press, 2004.
Ranta A. Type-Theoretical Grammar. Oxford: Oxford University Press, 1994. 240 p.
Ranta A. Grammatical Frameworks: A Type-Theoretical Grammar Formalism // The Journal of Functional Programming. 2004. Vol. 14. No. 2. P. 145–189.
Schneider L. The Logic of the Ontological Square // Studia Logica. 2009. Vol. 91. No. 1. P. 25–51.
Simons P. Particulars in Particular Clothing: Three Trope Theories of Substance // Philosophy and Phenomenological Research. 1994. Vol. 3. No. 54. P. 553–575.
Smith B. Against Fantology // Experience and Analysis / Eds. by J.C. Marek, M.E. Reicher. Vienna: Obv&Hpt, 2005. P. 153–170.
Sundholm G. Proof Theory and Meaning // Handbook of Philosophical logic III: Alternatives to Classical Logic / Eds. by D. Gabbay, F. Guenthner. Reidel. 1986. P. 471–506.
Sundholm G. Constructive Generalized Quantifiers // Synthese. 1989. Vol. 79. No. 1. P. 1–12.