Structured Properties and Propositions: Foundations and Applications

Numerous philosophers are committed to fine-grained accounts of properties, propositions, and relations. One approach gaining traction in recent decades is the structuralist view, which claims that properties and propositions with distinct constituents are distinct. However, the Russell-Myhill paradox has been proposed as evidence that this view is inconsistent within higher-order logic. Based on the previous work of other philosophers, my article-based dissertation is dedicated to the conceptual foundation and mathematical implementation of a framework, called generativism, which aims to retain the structuralist view and counter the paradox in a well-motivated way. Generativism is grounded on the idea that structured entities are iteratively generated, thereby circumventing the paradox. According to this view, the universe of structured properties and propositions is never fully available, but continuously expands through a hierarchy of stages. The key aspect of my approach is advocating for a predicative turn in higher-order logic, suggesting that the quantifiers used when generating new entities should only range over entities available at each stage of the generative process. So, the main aim of my dissertation is to propose a more thoroughgoing study of predicativism in the context of structured properties and propositions. I develop and discuss two mathematical implementations of these ideas. One is historically well-known in the logical and philosophical literature on predicativity: it is Russell's ramified theory of types. The other is Boolos' stage theory, which has received significant attention in the philosophy of set theory, but its applicability for structured propositions has been seriously underestimated. Ramified type theory is often deemed clunky and not explanatory, so my preferred approach for giving formal precision to generativism is the stage theory. The reason is that it provides greater flexibility, enhanced clarity, stronger theoretical justification, and a more streamlined framework, by bypassing the complications tied to ramified types and the use of modal operators, which are typical of potentialist views.