Four Theories of the Theory of Science: Husserl and Martin-Löf, Weyl, Cavaillès, Ladrière, Carnap and Awodey

By Eric Schmid

Abstract. This essay compares four ways of answering the question that Husserl called Wissenschaftslehre: what grounds the objectivity of the formal sciences, and what is philosophy’s task with respect to them? I read Husserl through the tradition that Per Martin-Löf has made contemporary—the semantics of evidence, judgement, and meaning explanation; Jean Cavaillès through Brice Halimi’s reconstruction of logic as the “science sought” and his dissociation of necessity from universality; Jean Ladrière through his interpretation of the limitative theorems; and Carnap through Steve Awodey’s double role as Carnap scholar and theorist of homotopy type theory. Hermann Weyl figures as the one mathematician who occupied every position in this field in turn—Husserlian evidence, Brouwerian construction, symbolic construction, and the principle of invariance. The essay argues that univalent foundations constitute an unplanned meeting point of the four programs: Martin-Löf’s Husserlian semantics of canonical evidence, Awodey’s Carnapian–structuralist principle of invariance, Cavaillès’s autonomous dialectic of the concept, and Ladrière’s thesis that every formalism remains internally open onto a horizon of sense.

1. Introduction: the question of the theory of science

There is a question that the analytic and phenomenological traditions inherited jointly from Bolzano and then answered apart: not what do the sciences know, but what is a science, such that it can know at all? Husserl’s name for the discipline that asks it was Wissenschaftslehre, the theory of science. In Lester Embree’s editorial formulation, the theory of science is the philosophical discipline that examines “the fields, relations, methods, categories, presuppositions, and grounds of the sciences” (Gurwitsch 1974, p. ix). The question is prior to epistemology in the modern sense, because it does not presuppose an inventory of established sciences whose reliability is then to be audited; it asks after the constitution of scientificity itself, and above all after the constitution of the formal sciences, logic and mathematics, which every other science presupposes.

Four answers to this question organize the present essay. The first is Husserl’s, in the radicalized and constructivized form it has taken in Per Martin-Löf’s type theory: the objectivity of logic and mathematics is grounded in evidence, in acts of demonstration whose meaning is fixed by what it would be to fulfil them. The second is Jean Cavaillès’s: no philosophy of consciousness, however transcendental, can deliver a doctrine of science; only a philosophy of the concept can, because the necessity that drives mathematics is the necessity of an autonomous dialectic, not of an activity of a subject. I will follow Brice Halimi’s reading of Cavaillès throughout. The third is Jean Ladrière’s: the limitative theorems of Gödel, Church, and Tarski are not a catastrophe for formalism but its most philosophically instructive product, showing that every formal system is constitutively open onto a horizon of operations and of sense that it cannot internalize. The fourth is Carnap’s: there is no question of grounding at all, only of choosing among linguistic frameworks under the principle of tolerance; and I will read Carnap through Steve Awodey, who is at once one of the finest historians of Carnap’s logic and one of the architects of homotopy type theory, in which, I shall argue, the Carnapian ideal of structural invariance is realized on a Martin-Löfian, which is to say a Husserlian, semantic base.

The polemical situation is thus not a simple two-party system, phenomenology against positivism. It is a four-cornered field, and one figure, Hermann Weyl, crossed it entire, beginning as Husserl’s most gifted mathematical disciple and ending as the theorist of invariance. The four corners have, in the last two decades, been drawn together by a single mathematical object: dependent type theory with the univalence axiom. That convergence was not designed by anyone; it is, in Cavaillès’s own vocabulary, an event in the autonomous becoming of the concept.

2. Husserl: the life-world, idealization, and the forgetting of origins

Aron Gurwitsch’s Phenomenology and the Theory of Science remains the most economical presentation of Husserl’s program in this domain, because Gurwitsch writes for non-phenomenologists and keeps the transcendental machinery in contact with actual mathematics and physics. Two theses organize the volume. First, scientific theories “derive from and ultimately refer back to the life-world” (Gurwitsch 1974, p. ix). Second, both the sciences and the life-world receive their final clarification only when considered as intentional correlates of acts of consciousness.

The first thesis is elaborated in Gurwitsch’s reconstruction of the Crisis. The universe of modern physics is not a datum but a construction, the correlate of specific conceptualizations (idealization, mathematization, algebraization, formalization), and these mental processes require pregiven materials on which to operate: the objects of everyday, prescientific experience. The life-world is therefore the Sinnesfundament, the foundation of sense, of Galilean science (Gurwitsch 1974, pp. 16–17). But this foundation has been systematically obscured. Since Galileo, the life-world has been overlaid with an Ideenkleid, a garb of mathematical ideas cast over it like a mask, so that something which is in truth a method, indeed the product of a method, has come to be taken for true being, while the one world actually given to us is demoted to a merely subjective appearance (Gurwitsch 1974, p. 17).

The mechanism of this forgetting is described with great precision in Gurwitsch’s essay on Galilean physics. Idealization is only the first step: after Galileo come the algebraization of geometry by Fermat and Descartes, the calculus of Leibniz and Newton, and finally the fully formalized disciplines of modern axiomatics, in which terms are divested of intuitive content and defined solely by the relations and operations in which they stand (Gurwitsch 1974, pp. 43–44). Formalization is the construction of algorithms: symbol systems on which operations can be performed blindly and mechanically. Such systems can be taught, transmitted, and perfected across generations without any reference back to their founding acts. The presuppositions of mathematical thought—life-world experience on one side, the operations of idealization and formalization on the other—“may and do fall into oblivion” (Gurwitsch 1974, p. 44). Severed from their sources, the formal disciplines appear autonomous, presuppositionless. Husserl calls this condition traditionality: proceeding on the basis of obfuscated and forgotten presuppositions. And Gurwitsch is careful to add that this proceeding is fully legitimate for the working mathematician; it is not the scientist’s job to interrogate the institution of his science. But: “It is the duty of the philosopher to raise precisely that question” (Gurwitsch 1974, p. 44).

The second thesis, the intentional-constitutive one, is what distinguishes Husserl’s theory of science from every merely historical or sociological genealogy of the formal. In the essay “Reflections on Mathematics and Logic,” a text taken from a manuscript of around 1950, Gurwitsch insists that the conditions of possibility of mathematics are not suppressed premises that could be restored to the deductive system; they “are not included in it as premises” at all (Gurwitsch 1974, pp. 60–61), and that is their mode of effectiveness. If logic and mathematics presuppose the world, they presuppose it not as an axiom but as “the nutritive matrix into which they plunge their roots” (Gurwitsch 1974, p. 75). And beyond the world, they presuppose consciousness directly: numbers, sets, propositions are ideal objects, identical correlates of open multiplicities of acts, and every operation by which such objects are formed is a step in thinking.

The decisive concept here, and the decisive one for Martin-Löf, is Husserl’s stratification of evidence in Formal and Transcendental Logic. The proposition that pure logic takes as its theme is the proposition given in the Evidenz der Deutlichkeit, the evidence of distinctness: the original apprehension in which the articulated unity of signification is itself present, a “conscious apprehension which is to the proposition what perception is to the material thing” (Gurwitsch 1974, p. 73). Distinctness concerns the proposition as such; the further evidence in which the proposition’s agreement with a state of affairs is itself given is the evidence of clarity, Evidenz der Klarheit. A word-series like “the sum of the angles of a triangle is equal to the color red” fails already at the level of distinctness: it has no ideal existence as a signification, and hence is not even a candidate for the logic of consequence (Gurwitsch 1974, pp. 73–74). Even the purest formal logic, in other words, tacitly grants that its symbols stand for terms that can cohere in one experienceable world. Evidence, finally, is not a regional curiosity of logic: every non-evident act refers to the evidence that would fulfil it, so that evidence has “a universal and teleological function in conscious life” (Gurwitsch 1974, p. 199). It is by following this chain of reflections that Husserl was led, as Gurwitsch notes with reference to FTL §§ 94 and 100, to the principle of phenomenological idealism: whatever exists and is valid derives its existence and validity from the conscious life in which it is given (Gurwitsch 1974, p. 76).

The Husserlian answer to the question of the theory of science is thus a two-storey structure of founding: the life-world below, constituting consciousness throughout. The philosopher’s task is the reactivation of the founding acts that traditionality has sedimented over.

3. Martin-Löf: the theory of science as constructive semantics

One might file this program under the history of a defeated school. But it was taken up, almost clause by clause, in the most technically consequential foundational system of the late twentieth century. Per Martin-Löf has been explicit about the lineage: his lectures on the meanings of the logical constants deploy Husserl’s vocabulary of act, object, and evidence, and his Synthese paper of 1987 bears a title that could serve as a table of contents for Formal and Transcendental Logic: “Truth of a Proposition, Evidence of a Judgment, Validity of a Proof” (Martin-Löf 1987; Martin-Löf 1996).

The central move of intuitionistic type theory (Martin-Löf 1984) is the restoration of a distinction that Frege’s assertion sign marked but that post-Fregean logic flattened: the distinction between proposition and judgement. A proposition is what can be true; a judgement is what can be known, made evident. The forms of judgement of type theory—A type, a : A, A = B, a = b : A—are not themselves propositions and do not have truth-values; they have correctness, and their correctness is a matter of demonstrability, of evidence. Martin-Löf’s meaning explanations then do for each form of judgement what Husserl’s doctrine of evidence demands: they say what one must know in order to have the right to make the judgement. To know a proposition A is to possess a proof-object a : A; and what counts as a proof-object of A is fixed by specifying the canonical proofs of A and the means of evaluating arbitrary proofs to canonical form. Meaning is given by the conditions of fulfilment.

These resonances go deeper than vocabulary. The relation between an arbitrary (non-canonical) proof-object and its canonical value is a formal double of the relation, described above, between a non-evident act and the evidence that fulfils it: every non-canonical expression refers to the canonical form to which it evaluates, exactly as every signitive intention refers to the intuition that would fulfil it. The evidence of distinctness reappears as the presupposition, in each judgement a : A, of the prior judgement A type: before anything can be evident of A, A itself must be grasped as a well-formed signification—the type-theoretic analogue of Gurwitsch’s point that the color-red pseudo-proposition never attains ideal existence (Gurwitsch 1974, pp. 73–74). And Martin-Löf’s analysis of the analytic and the synthetic in type theory (Martin-Löf 1994)—the judgement a : A is analytic in the sense that it contains its own grounds, whereas the demonstration that produces a may be as synthetic, as constructive, as one pleases—rehearses Husserl’s insistence that logic’s ideal objects are at once atemporal in validity and generated in acts with an intentional history.

Two consequences matter for what follows. First, Martin-Löf’s theory of science is normative through and through: logic is not a description of reasoning but the articulation of the demands—the “ought”—internal to knowing. The theory of science becomes a theory of scientific acts and of what entitles them. Second, the ground so provided is open: because the meaning explanations are semantical rather than formal, the theory escapes the fate that Cavaillès (and, differently, Ladrière) read out of Gödel’s theorems for Hilbert’s program. There is no pretension to a closed system whose consistency certifies itself; there is only the unbounded reactivability of evidence. In this sense Martin-Löf is the executor of the Husserlian testament: the duty of the philosopher, to reactivate the founding acts beneath the algorithm, has been discharged inside mathematics, as its semantics, and not in a commentary upon it.

4. Weyl: a mathematician’s transit through all four quadrants

Before turning to Husserl’s great French critic, I want to pause over the one working mathematician of the first rank who inhabited this entire problem-space from the inside: Hermann Weyl. Weyl is not a fifth doctrine so much as the field’s living diagram. Over four decades he occupied, in turn, each of the positions this essay distinguishes, and the pressures that moved him from one to the next are the best evidence we have that the positions really do communicate.

He began as a Husserlian, and militantly so. Das Kontinuum of 1918 (Weyl 1918) opens under the explicit patronage of phenomenology—Weyl had absorbed Husserl at Göttingen, and the correspondence between the two, published by van Dalen, shows Husserl reading Weyl’s forays into foundations with delighted recognition (van Dalen 1984). The book’s mathematical content is a rigorously predicative reconstruction of analysis: only those sets of reals exist that are arithmetically definable from below, without the vicious circle of quantifying over a totality in the course of defining one of its members. The philosophical motivation is Gurwitsch’s “duty of the philosopher”: to refuse the traditionality of classical analysis, whose set-theoretic continuum proceeds on presuppositions that have “fall[en] into oblivion” (Gurwitsch 1974, p. 44), and to rebuild the edifice from operations whose sense can be made present. Three years later, in the paper that named the Grundlagenkrise (Weyl 1921), Weyl radicalized this into an open embrace of Brouwer: the continuum as a medium of free becoming, choice sequences, the rejection of the completed infinite. In hindsight the trajectory from Das Kontinuum through the Brouwerian episode runs straight toward Martin-Löf: predicativity is a design constraint of intuitionistic type theory, whose universes are stratified to avoid the circles Weyl diagnosed, and the meaning-theoretic demand that every assertion be backed by an exhibitable construction is the demand of 1921 made systematic. Weyl is, in this respect, the missing link between §2 and §3 of this essay, the first person to try to be a Husserlian constructivist in full mathematical earnest.

But he did not stay. Under the pressure of physics and of Hilbert’s counterattack, the later Weyl conceded that the mathematics actually needed by science outruns what intuition can fulfil, and he re-described mathematics as symbolic construction: a free, creative, sign-mediated practice whose individual formulas no longer carry intuitive sense one by one, and which is answerable to experience only as a whole, in the company of physics (Weyl 1949). This is an intermediate position, and its neighbors are instructive. It concedes to Carnap that the system, not the single evident act, is the unit of significance; it retains against Carnap the conviction that the symbolic apparatus remains about something—that theoretical construction is a mode of access to the world, not a framework floating on a convention. And in its insistence that mathematics develops by an inner drive of its symbolic forms, each construction motivating the next, it stands close to the dialectic of concepts that Cavaillès, who had studied the Grundlagenkrise debates among Brouwer, Weyl, and Hilbert closely in his 1938 theses, was formulating at the same moment. Even Weyl’s farewell to phenomenology was staged inside it: his contribution to the 1940 Husserl memorial volume, “The Ghost of Modality” (Weyl 1940), subjects the modal notions of necessity and possibility to a logician’s exorcism, dissolving them into the machinery of implication and construction—an affectionate parricide, performed at the master’s own commemoration, of the idea that a phenomenology of essences could legislate for logic.

There is finally the Weyl of invariance, and he is the one who matters most for §7 below. From the Erlangen inheritance through Philosophy of Mathematics and Natural Science to the luminous last book Symmetry, Weyl made one idea central: “objectivity means invariance with respect to the group of automorphisms” (Weyl 1952, p. 132). What is real in a structured domain is what all structure-preserving transformations agree on; the substrate points, in themselves, are nothing. This is the principle Awodey identifies as the content of structuralism and that univalence writes into the grammar of the language. The line of descent Klein–Weyl–Mautner–Tarski–Awodey is explicit in the literature of univalent foundations; what is less often said is that the man who forged its central maxim was the same man who had begun by trying to build analysis on Husserlian evidence. That both commitments could live in one mathematician—evidence at the base, invariance at the summit—is a biographical anticipation of the synthesis I will claim, in §8, that homotopy type theory effects doctrinally.

5. Cavaillès: from the philosophy of consciousness to the philosophy of the concept

Jean Cavaillès wrote Sur la logique et la théorie de la science in 1942, in a military prison at Montpellier, between two arrests; he was shot by the Gestapo in 1944, and the text appeared posthumously in 1947 (Cavaillès 1947). It is the most compressed and the most devastating examination that Husserl’s theory of science ever received from a reader who had absorbed it completely. Cavaillès takes the question in the form we have given it—what can a doctrine of science be?—and runs it through Kant, Bolzano, Brunschvicg, Carnap, and finally Husserl, whom he treats as the deepest of the available options because transcendental logic promises what the others cannot: an account of how the formal disciplines are generated and not merely described.

The objection is structural, not textual. If formal logic is to be grounded in transcendental logic—in the constituting acts of a subjectivity—then either the transcendental analysis itself borrows its organon from the very logic it is supposed to ground, and the foundation is circular; or transcendental subjectivity is genuinely prior and autonomous, in which case its necessities are those of an activity, and nothing guarantees that the contents generated will carry the unconditional, ever-growing, self-correcting necessity that mathematics in fact displays. Husserl’s absolute consciousness, Cavaillès argues, can found the sciences only by absorbing their content into itself; but the actual history of mathematics shows content outrunning every act that was supposed to constitute it. Gödel’s incompleteness results function in the argument as the mathematical emblem of this excess: no fixed system—and, by extension, no fixed inventory of constituting acts—closes over what mathematics will have become. Demonstration is not the execution of a program laid down in advance by consciousness; it is an event in which the concept reorganizes itself. Hence the famous conclusion, in the book’s final lines: a doctrine of science can be furnished not by a philosophy of consciousness but by a philosophy of the concept. “The generative necessity is not that of an activity, but of a dialectic” (Cavaillès 2021, p. 136).

What Cavaillès left at his death was less a doctrine than a demand, articulated through two operators that he had isolated in his earlier historical work on set theory and axiomatics: paradigmatization, in which a determinate mathematical gesture is varied until its form detaches as a new object, and thematization, in which an operation previously merely exercised becomes itself the theme of a higher theory—the group of transformations studied as a structure, the proof studied by proof theory. Mathematics advances by this self-engendering, and the necessity of the advance belongs to the chain of concepts itself, not to any subject, empirical or transcendental, who follows it. One begins to see why category theorists have always felt that Cavaillès was describing them before the fact: adjunctions, representability, the passage from a construction to the functor it determines, are thematization made algebra. The philosophy of the concept was a philosophy in search of its mathematics, and the mathematics arrived within a decade of the author’s death.

Halimi as reader of Cavaillès

Brice Halimi’s reading intervenes here, and its merit is to take seriously what the French reception of Cavaillès, from Canguilhem to Foucault, too often treated as a mere slogan. In his article “La logique, science recherchée” (Halimi 2020), Halimi starts from the observation that the theory of science Cavaillès is looking for—his epistēmē zētoumenē, the “science sought” in the Aristotelian sense—would have to permit a systematic study of forms; and Cavaillès finds it nowhere. Not in the Kantian analytic, not in Bolzano’s Wissenschaftslehre, not in Frege, Carnap, or Tarski, not in Hilbertian proof theory, and not in the Husserlian mathesis universalis. Each candidate fails for the same deep reason: each freezes form—as category, as syntax, as the structure of a closed system—where the Cavaillèsian demand bears on the engendering of forms one from another. Halimi’s own, deliberately provocative thesis is that Cavaillès could have approached the logic he sought had he paid more attention to a figure he neglected: Russell, and Russell’s heir Wittgenstein; that is, an analysis of the notion of form itself, whether form designates a symbolic complex, a mathematical structure, or a demonstrative schema.

But it is Halimi’s principal book, Le nécessaire et l’universel (Halimi 2013), crowned fittingly with the Prix Cavaillès, that provides, to my mind, the best systematic commentary on the “generative necessity.” The philosophical tradition from Kant to Tarski admitted without discussion a correlation between necessity and universality: the necessary would be what is true in all possible cases. Halimi contests the presupposition. Correlated, the universal and the necessary each refer back to a totality of possibles whose origin remains unexplained; thought separately, each can instead be understood in its genesis. The universal is to be rethought in terms of genericity—the intersubstitutability of the elements of a universe being contemporaneous with the constitution of that universe, not prior to it—while the necessary is defined by reference to a possible that is neither totalizable nor reducible to a single plane. The Cavaillèsian import of this double dissociation is immediate. The necessity Cavaillès speaks of, the one that chains concepts together in mathematical becoming, was never the logical universality of truths valid in all possible worlds; it is a step-by-step, local, and productive necessity, the constraint a problem exerts on its solution and a structure on its prolongations. By dissociating the two notions, Halimi gives Cavaillès’s “dialectic” what it lacked: a modal framework in which mathematical necessity can be genetic without ceasing to be necessity, and in which the universality of structures is the result of generic procedures rather than their presupposition. The philosophy of the concept ceases to be an anti-Husserlian slogan and becomes a program: to describe, with mathematical means—Halimi readily mobilizes the geometry of fibered spaces and, elsewhere, fibered semantics—the way domains of objects and their laws are constituted together.

Against Husserl and Martin-Löf, Cavaillès and Halimi deny that acts and their evidence can be the ultimate bearers of mathematical necessity: evidence is always evidence within a conceptual situation that no act instituted. Against Carnap, they deny that the choice of framework is philosophically primitive: frameworks themselves are generated, paradigmatized, thematized, and the logic of that generation is exactly what a theory of science must state. The philosophy of the concept is thus the standing challenge to both semantic foundationalism and syntactic conventionalism.

6. Ladrière: the internal limitation of formalisms and the horizon of sense

Jean Ladrière occupies a mediating position in this field, and he occupied it knowingly. A Louvain philosopher formed equally by the Husserl archives and by mathematical logic, he published in 1957 the first comprehensive philosophical study of the limitative theorems: Les limitations internes des formalismes, on the significance of Gödel’s theorems and their kin—Church, Tarski, Löwenheim–Skolem—for the foundations of mathematics (Ladrière 1957). The title contains the thesis. The limitations of formalism are internal: they are not objections brought against formal method from outside, by intuitionist scruple or phenomenological nostalgia, but theorems that formal method proves about itself, with full formal rigor. Formalization, pushed to its own ideal of completeness and self-certification, generates the exact demonstration that the ideal is unattainable.

Where Cavaillès reads this excess as the sign that necessity belongs to the concept’s dialectic rather than to any subject, Ladrière draws a more Husserlian moral, though one chastened by Cavaillès. A formal system, he argues, is essentially an instrument: the sedimented deposit of operations of an effective, temporally unfolding mathematical thought. The limitative theorems demonstrate that the deposit can never absorb the operating. Every formalism determines, beyond what it can derive, a fringe of statements and of notions—its own consistency first among them—that are visible from the system, formulable about the system, and undecidable within it; mastering them requires ascending to another system, which reproduces the situation. Formal thought is thus constitutively open: it points beyond each of its crystallizations toward an inexhaustible horizon of further operations. The word horizon is chosen deliberately. What Husserl described noetically—every givenness surrounded by co-given potentialities, every evidence referring beyond itself—Ladrière finds again as a metamathematical structure. The limitative theorems are the life-world’s revenge stated in arithmetic: the proof that the Ideenkleid cannot be woven shut, that the garb of ideas necessarily gapes, and that through the gap one sees the operating intentionality that Gurwitsch said had fallen “into oblivion” (Gurwitsch 1974, p. 44).

In his later work, above all L’articulation du sens (Ladrière 1970–84), Ladrière generalized this into a philosophy of language and of science: formal systems, natural languages, and even theological discourse are so many regimes of the articulation of sense, each effective precisely because none is total. For the theory of science this yields a position of principled modesty that neither Husserl nor Carnap could quite endorse: foundations are real but always partial; the ground is touched operation by operation, never surveyed. Ladrière thereby anticipates the actual epistemic situation of contemporary foundational practice, in which one works inside a system (a type theory, a topos, a set theory) whose metatheory one holds open, and in which the interesting properties—normalization, canonicity, consistency—are established relative to yet further systems, without vertigo and without ground-floor. He is the philosopher of the fact that this is not a scandal.

7. Carnap and Awodey: tolerance, invariance, univalence

Carnap is absent from Gurwitsch’s anthology, but his position is the unnamed target of its final essay, which opens with a critique of “the unity of science movement”: the elevation of the method of physics into the scientific method, with verification restricted to what is public, that is, accessible “by means of mere sense perception,” and the consequent decision—methodological before it is ontological—that consciousness and meaning are not possible subject matters of science (Gurwitsch 1974, pp. 132–33). Gurwitsch’s complaint is that here a method dictates to the regions of being rather than deriving from them. It is the Crisis argument transposed: once again a method is taken for true being.

Yet this physicalist Carnap is the shallowest of the available Carnaps, and Steve Awodey’s historical work has done much to recover a deeper one (Awodey & Carus 2001; Awodey & Klein 2004). The Carnap of the Aufbau (Carnap 1928) is engaged in a constitution theory, Konstitutionstheorie, whose debts to Husserl are structural and documented: a stepwise construction of the objectivities of science from lived experience, with the express aim of exhibiting objectivity as invariance of structure, the purely structural definite description that holds regardless of the intrinsic qualities of the basis. The Carnap of the Logical Syntax (Carnap 1934) then executes the great renunciation: the principle of tolerance. In logic there are no morals; everyone is free to build his own language; the philosopher’s task is not to ground the framework but to state, with exactness, the consequences of adopting it. Philosophy survives as Wissenschaftslogik, the logic of science—the same genitive as Wissenschaftslehre, with the doctrine deleted. External questions about the correctness of a framework are not false but empty; what remains are internal questions, and pragmatic comparisons of frameworks (Carnap 1950). Awodey and Carus have shown how hard-won this position was: Carnap’s pre-Gödelian ambition of a universal, categorical characterization of mathematical truth (the Gabelbarkeitssatz of 1928) collapsed under the incompleteness theorems, and tolerance was the philosophically creative response—where Cavaillès responded to the same theorems with the dialectic of the concept, and Ladrière with the open horizon (Awodey & Carus 2001).

Awodey’s second life is as a category theorist and a founder of homotopy type theory, and the continuity with his Carnap scholarship is more than biographical. In “Structuralism, Invariance, and Univalence” (Awodey 2014), he argues that the univalence axiom of Voevodsky—identifying identity of types with equivalence of types—finally gives exact mathematical form to the structuralist principle that isomorphic objects are identical, that is, that nothing meaningful can be said of a mathematical object beyond what is invariant under equivalence. In univalent foundations one literally cannot formulate the structure-transcendent questions; the language enforces invariance the way Carnap dreamed the logic of science would dissolve metaphysics: not by prohibition but by construction. Tolerance, too, returns with a precise face: type theories are a plurality of frameworks, compared by interpretability and semantics, adopted for their expedience, their metatheory pursued without any pretense that one of them is written into the nature of things.

But here the dialectical joke of the situation becomes audible. The formal substrate of homotopy type theory is Martin-Löf’s intuitionistic type theory (Univalent Foundations Program 2013). The system in which Awodey’s Carnapian–structuralist ideal of invariance is realized is the system whose meaning explanations are the most Husserlian semantics ever given to a formalism: judgement, evidence, canonicity, fulfilment. The identification of identity with equivalence is carried by identity types, whose meaning explanation—what counts as evidence for an identification—is just the kind of intentional-semantic clause that the Syntax program had banished. Univalent foundations are, taken as a whole, a Husserl–Carnap chimera: constitution theory above, evidence theory below.

8. Conclusion: the four programs at the type-theoretic present

To the question—what grounds the objectivity of the formal sciences?—Husserl answers: constituting consciousness and its evidences, forgotten beneath sedimented tradition and recoverable by reactivation; Martin-Löf shows that the answer can be engineered, made internal to mathematics as a semantics of judgement. Cavaillès answers: nothing subjective grounds it; the necessity is the concept’s own generative dialectic, and Halimi shows that this necessity can be thought rigorously once it is dissociated from logical universality and referred to genericity and to a non-totalizable possible. Ladrière answers: the ground is real but structurally unreachable; every formalism proves from within that it opens onto a horizon it cannot close. Carnap answers: the question is empty; choose your framework tolerantly and do the logic of science; Awodey shows that the deepest form of this answer is not physicalism but invariantism, consummated in univalence. And Weyl, who gave no single answer, gave instead the itinerary: from evidence to construction to symbol to invariance, each station forced by honest pressure from mathematics and physics, none ever fully renounced.

I close with a claim: dependent type theory with univalence is the first mathematical object adequate to all four answers at once, and its adequacy is the strongest available confirmation of Cavaillès. Its semantics is Husserlian: meaning explanations, evidence, the reference of every expression to canonical fulfilment. Its ontology is Carnapian and Weylian: invariance enforced by construction, objectivity as what the automorphisms preserve, frameworks held tolerantly. Its predicative discipline of stratified universes is Weyl’s constraint of 1918 made architecture. Its metatheory is Ladrièrian: normalization, canonicity, and consistency are pursued from outside, system by system, with Gödelian openness accepted as the permanent condition. And its history is Cavaillèsian: no one intended this synthesis. Identity types were a technical device of 1972; their homotopical meaning was discovered, not designed, thirty years later; the concept, varied and thematized—identity paradigmatized into path, equivalence thematized into univalence—reorganized the field over the heads of every school. The theory of science that Husserl demanded, Cavaillès radicalized, Ladrière tempered, and Carnap renounced is being written; but it is being written the way Cavaillès said it would be: not by a consciousness, however transcendental, but by a dialectic. The duty of the philosopher that Gurwitsch named—to raise the question of origin and institution that the working scientist rightly brackets—remains; only now the origins to be reactivated include the acts of the concept itself.

References

Awodey, S., and A. W. Carus. “Carnap, Completeness, and Categoricity: The Gabelbarkeitssatz of 1928.” Erkenntnis 54 (2001): 145–172.
Awodey, S., and C. Klein, eds. Carnap Brought Home: The View from Jena. Chicago and La Salle: Open Court, 2004.
Awodey, S. “Structuralism, Invariance, and Univalence.” Philosophia Mathematica 22, no. 1 (2014): 1–11.
Carnap, R. Der logische Aufbau der Welt. Berlin: Weltkreis, 1928.
Carnap, R. Logische Syntax der Sprache. Vienna: Springer, 1934.
Carnap, R. “Empiricism, Semantics, and Ontology.” Revue Internationale de Philosophie 4 (1950): 20–40.
Cavaillès, J. Sur la logique et la théorie de la science. Paris: Presses Universitaires de France, 1947; repr. Paris: Vrin, 1997.
Cavaillès, J. On Logic and the Theory of Science. Translated by Knox Peden and Robin Mackay. Falmouth: Urbanomic / Sequence Press, 2021.
Gurwitsch, A. Phenomenology and the Theory of Science. Edited by Lester Embree. Evanston: Northwestern University Press, 1974.
Halimi, B. Le nécessaire et l’universel: analyse et critique de leur corrélation. Paris: Vrin, 2013.
Halimi, B. “La logique, science recherchée.” Revue de Métaphysique et de Morale 106, no. 2 (2020): 145–164.
Husserl, E. Formale und transzendentale Logik. Halle: Niemeyer, 1929.
Husserl, E. The Crisis of European Sciences and Transcendental Phenomenology. Translated by David Carr. Evanston: Northwestern University Press, 1970.
Ladrière, J. Les limitations internes des formalismes: étude sur la signification du théorème de Gödel et des théorèmes apparentés dans la théorie des fondements des mathématiques. Louvain: Nauwelaerts / Paris: Gauthier-Villars, 1957.
Ladrière, J. L’articulation du sens. 2 vols. Paris: Cerf, 1970–1984.
Martin-Löf, P. Intuitionistic Type Theory. Notes by Giovanni Sambin. Naples: Bibliopolis, 1984.
Martin-Löf, P. “Truth of a Proposition, Evidence of a Judgment, Validity of a Proof.” Synthese 73 (1987): 407–420.
Martin-Löf, P. “Analytic and Synthetic Judgements in Type Theory.” In Kant and Contemporary Epistemology, edited by Paolo Parrini, 87–99. The University of Western Ontario Series in Philosophy of Science 54. Dordrecht: Kluwer, 1994.
Martin-Löf, P. “On the Meanings of the Logical Constants and the Justifications of the Logical Laws.” Nordic Journal of Philosophical Logic 1, no. 1 (1996): 11–60.
van Dalen, D. “Four Letters from Edmund Husserl to Hermann Weyl.” Husserl Studies 1 (1984): 1–12.
Sinaceur, H. Cavaillès. Paris: Les Belles Lettres, 2013.
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton: Institute for Advanced Study, 2013.
Weyl, H. Das Kontinuum: Kritische Untersuchungen über die Grundlagen der Analysis. Leipzig: Veit, 1918.
Weyl, H. “Über die neue Grundlagenkrise der Mathematik.” Mathematische Zeitschrift 10 (1921): 39–79.
Weyl, H. “The Ghost of Modality.” In Philosophical Essays in Memory of Edmund Husserl, edited by Marvin Farber, 278–303. Cambridge, MA: Harvard University Press, 1940.
Weyl, H. Philosophy of Mathematics and Natural Science. Princeton: Princeton University Press, 1949.
Weyl, H. Symmetry. Princeton: Princeton University Press, 1952.