Things, Properties, Relations in Type-Theoretical Ontology

Abstract

Thing, property and relation from ancient to present times belong among fundamental ontological categories. Starting from Frege logic describes properties and relations uniformly as n-placed predicates and type theory often follows this course. However, their traditional understanding not only leads to problems and paradoxes but also goes against ontological intuitions of type theory itself. The article examines the traditional presentation of properties and relations in type theory and their alternative formalization which prevents the hypothetical emergence of any «thing without properties». Type theory is considered as not merely logical but also ontological system. It is argued that the common presentation of properties as types dependent on objects follows the description model of relations and becomes inadequate when applied to the things as such. Simple examples of formalizations in the language Lean are provided. The sense in which this formalization fits better the ontological foundations of type theory is described.