What Comes First? Mathematical Objects or Their Logical Justification? A Type-Theoretic Perspective for Mathematics Education

Mathematics education has studied how learners come to conceive processes as mathematical objects. Mainstream logical semantics, by contrast, normally starts after such objects are already available: in standard model-theoretic semantics, quantified statements are evaluated relative to a given domain. This essay explores the tension between these two perspectives. It asks whether type theory offers a useful formal vocabulary for describing the constitution of mathematical domains prior to reasoning about them. Inductive types provide a particularly transparent example: the natural numbers are specified through rules for forming and using their elements rather than by first postulating a completed domain. Yet induction is not general enough to account for all mathematical object formation. Herbrand universes and the contrast between the real algebraic numbers and the real numbers illustrate both the power and the limitations of term-generated domains. Dependent type theory suggests a broader perspective in which new domains arise through type formation—including function types, dependent types, inductive types, and suitable quotient constructions. The proposal is not that type theory is a psychological theory of learning, but that it may provide a normative formal counterpart to didactical theories of object constitution such as Sfard’s process–object duality and APOS theory.