The Forced Operational Ordering of Logic, Sets, Types, and Categories: The Foundations of Mathematics

Abstract

Any mathematical construction requires four operations to be performed in a fixed structural order. The four operations are distinction, placement, identity, and composition. Logic formalizes distinction, sets formalize placement, types formalize identity, and categories formalize composition. Each foundation formalizes one operation as primary and employs the remaining three as apparatus. The four operations proceed in the order distinction, placement, identity, composition, and that order is forced by operational dependency. The bilateral correspondences established by Curry and Feys (1958) and Howard (1969/1980), extended by Lambek (1972), and connected to sets through topos theory by Lawvere (1970) and Tierney (1972) are cited as the published evidence that each of the four foundations has the capacity to express all four operations as a single formal system. In this sense each foundation is four-in-one, and the four foundations are structurally translatable into one another. The contribution of this paper is the recognition that the four operations, contained as one in each foundation, proceed in a fixed dependency order, with distinction preceding placement, placement preceding identity, and identity preceding composition. The bilateral correspondences are symmetric. We propose the dependencies among the four operations are not symmetric, and the asymmetry of the dependencies fixes the direction in which the correspondences are used when a construction is built up. The correspondences themselves remain equivalences. We distinguish the operations any mathematics must perform from the axiomatic apparatus chosen as primary. The existing foundational debates (ZFC versus Martin-Löf type theory versus ETCS) concern which apparatus is primary and do not address the question we ask. The claim is falsifiable. A piece of mathematics that genuinely lacks one of the four operations would refute it. We predict no such piece exists, because the four operations are features of any mathematical construction. **Keywords:** foundations of mathematics, philosophy of mathematics, Curry-Howard correspondence, Lambek correspondence, topos theory, propositions-as-types, logic, set theory, type theory, category theory, ETCS, mathematical structuralism