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

This paper proposes that 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, set theory formalizes placement, type theory formalizes identity, and category theory formalizes 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 set theory through topos theory by Lawvere (1970) are cited as the published evidence that the four foundations are structurally translatable into one another. The contribution of this paper is the recognition that the four operations proceed in a fixed dependency order, with distinction preceding placement, placement preceding identity, and identity preceding composition. The bilateral correspondences are symmetric. We argue the dependencies among the four operations are not symmetric, and the asymmetry of the dependencies breaks the symmetry of the correspondences and fixes the direction. We distinguish the operations any mathematics must perform from the axiomatic apparatus chosen as primary. The existing foundational debates (ZFC versus 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 argue no such piece exists, because the four operations are features of any mathematical construction. **Keywords:** foundations of mathematics, four operations, distinction, placement, identity, identification, composition, forced operational ordering, Curry-Howard correspondence, Lambek correspondence, topos theory, propositions-as-types, operational dependency, endomorphism, logic, set theory, type theory, category theory