PhilMath Intersem 6.2015

The sixth annual PhilMath Intersem (PhilMath Intersem 6) will take place this coming June (June 2015).

The theme will be the nature and role(s) of construction in mathematics.

There will be eight meetings of the seminar this year.

Meeting dates are June 2nd, June 4th, June 9th, June 11th, June 16th, June 18th, June 23rd and June 25th.

Some sessions are single sessions (one presentation and discussion), some double (two presentations and two discussions).

All meetings will take place on the Rive Gauche campus of the University of Paris 7-Diderot, in the salle Klimt (room 366A) of the Condorcet Building.

The PhilMath Intersem is jointly sponsored by the history and philosophy of science department of the University of Paris 7-Diderot, the University of Notre Dame, the SPHERE group of the University of Paris 7-Diderot and the Archiv Henri Poincaré (AHP) of the University of Lorraine.

See the schedule below for further information, including titles, summaries and suggested readings.


Meeting 1: Tuesday, June 2nd, 16h00

Göran Sundholm (University of Leiden), "Constructions in Constructive Mathematics and Logic"


In this talk I will focus on construction as it figures in Constructive Mathematics.

On merely linguistic grounds one would expect constructive mathematics and logic somehow to involve constructions, and this is the case. Already in his earliest writings on the topic, when explaining the notion of proposition that serves in his formalized system of logic from a couple of years earlier, Arend Heyting held that a proof of a proposition is a mathematical construction that satisfies certain conditions and that can itself be considered mathematically. Drawing upon work by Kolmogoroff, who interpreted the constructive logical calculus in terms of tasks or problems and the mathematical proofs as their solutions, Heyting also, as is well-known, gave clauses for the logical connectives and quantifiers that have later been given a streamlined form that has come to be known as BHK. Heyting also knew of Gentzen’s Natural Deduction formulations of formal systems and used them in exposition of mathematical intuitionism.

In my lecture I want to give an overview of how the logical community reacted to the notion of a construction as a proof of a proposition. This is a notion novel with Heyting: previously all demonstration had taken place at the level of theorems, but now proofs pertain also to entities at the level of propositions, that is, contents of theorems. Several of the foremost foundational researchers confronted the issue: Gödel, for instance, had a lifelong interest in the matter (1933 talk, Zilsel lecture, and the various formulations of the Dialectica interpretation), but never reached a satisfying position. Stephen Kleene (recursive realizability) and Georg Kreisel (Theory of Constructions at LMPS I at Stanford) also engaged intensively with the issues. Gödel and Kreisel thought of constructions as being given in a universe of all constructions, a totality which, in Gödel's words, is a ”vast totality”.

Expanded summary: gs.summary.constructions_in_constructive_mathematics_and_logic.pdf


Sundholm, G., "Constructions, Proofs and the Meaning of the Logical Constants", Journal of Philosophical Logic 12.2 (1983): 151-172.

Weinstein, S., "The Intended Interpretation of Intuitionistic Logic", Journal of Philosophical Logic 12.2 (1983): 261-270.

Meeting 2: Thursday, June 4th, 16h00

David Rowe (Johannes Gutenberg University, Mainz), "Reflections on the Role of Construction in Hilbert's Grundlagen der Geometrie"


In his polemical arguments with Frege, Brouwer, and the ghost of Kronecker, Hilbert took the position that one did not need to construct a mathematical object in order to claim its existence. In particular, he hoped to show that the existence of the real number continuum could be proved by showing that the axioms used to characterize it were consistent. That famous program, already implicit in his Grundlagen der Geometrie of 1899, became explicit the following year when he formulated the second Paris problem.

Yet, notwithstanding the centrality of these debates, one should not jump to the conclusion that Hilbert was indifferent about issues of constructibility. These often played a key role in his works, including Grundlagen der Geometrie. However, there he postponed the discussion of construction problems to its seventh and final chapter, which will serve as the focal point for my argument. Indeed, I will offer a different sort of reading of this classical text in order to show the implicit relevance of construction issues for the way Hilbert proved the consistency of his axiom system in chapter 2. Afterward, I will indicate how construction issues played an even more transparent role in work done by some of Hilbert’s students. After briefly describing this side of Hilbert’s foundational interests, I conclude by suggesting a larger framework in which questions about constructability and decidability helped frame his more mature epistemological views.


Hilbert, D., Grundlagen der Geometrie, chs. 1, 2 and 7.

Hilbert, D., Hilbert.1919_20.pdf (Natur und mathematisches Erkennen).

Meeting 3: Tuesday, June 9th, 14h00

Gilles Dowek (INRIA, Deducteam), "A radical view of proofs as algorithms: certifying vs. certified algorithms"


The difficulty of proving some algorithms correct has led to the development of a new methodology
where the algorithms are not proved to always produce a correct result, but are required,
at each execution, to provide a proof of the correctness of the result produced during this
particular execution. This difference between certified and certifying algorithms leads to
revisit an old question about the algorithmic interpretation of proofs: how do we know
that an algorithm is a proof of a given proposition?


Dowek, G., Proofs in Theories, sections 8.1.3 and 8.1.4.

Necula, G. & P. Lee, "Design and Implementation of a Certifying Compiler", introduction.

Meeting 4: Thursday, June 11th. Double Session.

Session 1. 14h00

John Bell (University of Western Ontario), "Hermann Weyl and Constructivism"


Weyl characterized the mathematical method as "the a priori construction of the possible in opposition to the a posteriori description of what is actually given."  In my talk I shall attempt to explicate what Weyl meant by "a priori construction" and go on to compare his conception of the constructive in mathematics with contemporary ideas on the subject.


Weyl, H., The Continuum.

Bell, J. & H. Korté, "Hermann Weyl", Stanford Encyclopedia of Philosophy

Bell, J., "Hermann Weyl on Intuition and the Continuum"


Session 2. 16h15

Carl Posy (Hebrew University of Jerusalem), "Intuition and Construction in the Foundations of Mathematics: Three Case Studies"


The initial two parts of my talk, which are exegetical case studies, aim to showcase the versions of mathematical intuition and of mathematical construction that characterize the constructivist attitude in mathematics and to crystallize the firm connection between these notions that marks constructivism.  Kant and Brouwer will be my model constructivists.  The third part, which is more speculative, aims to drive a wedge between these notions.  I will try to do this by showing that contemporary category theory, though generally non-constructive, nevertheless encodes a legitimate and full scale notion of mathematical intuition.

For Kant and Brouwer, intuition is of course a cognitive notion; but it is also an epistemic one: knowledge ultimately rests on intuitions.   In the first part of the talk I will show how Kant’s notion of mathematical intuition distills out some formal elements of his conception of empirical intuition (perception), and how in particular his notion of mathematical construction relates to the theory of “empirical synthesis” that underlies his view of empirical intuition. I will show how in both the empirical and the mathematical cases Kant’s conception of intuition is not only cognitive and epistemic; it is also intertwined with ontological and semantic doctrines. Ontologically, intuitions – and only intuitions – give grounds for existence and identity claims; and semantically, for Kant, the possibility of intuition grounds truth and meaning.

I believe that aspects of this Kantian picture underlie each of the different 20th Century constructivist movements; including, indeed a connection to some notion of construction and also some version of the nexus with ontology and semantics.  But, as I said, my second case study will focus exclusively on Brouwer’s intuitionism. I will look at Brouwer’s deviations from Kant as well as his common points.   From this comparison I will distill those assumptions which, I believe, characterize the contemporary picture of mathematical intuition.  Chief among those assumptions is that the identity and existence of objects ultimately rest on the composition of the objects, and thus that intuition must somehow reflect that composition.   Constructivists demand that this composition be finitely (or humanly) graspable.  Non-constructivists, who drop this demand, also drop the demand for intuitive foundations.

I will start the third case study by sketching a different notion of intuition altogether, one that is, perhaps closer to the ‘common sense’ understanding of that term.  This is a notion of practical, or skill-related, rather than epistemic intuition; and I will argue that in its initial stages category theory targets the mathematical avatar of that practical intuition.   But in its later stages, I shall claim, category theory encapsulates a more subtle and more general non-epistemic attitude.  I will show which of the Kant-inspired characteristics of intuition this new notion preserves, and thus why it counts as a full scale notion of mathematical intuition.  But I will show that in particular it abandons the compositionality assumption. And that will be why this notion of intuition is non-constructive (actually, I will say, a-constructive).

If there is time I will conclude with a brief coda which relates this way of thinking about mathematical intuition to some contemporary debates about category theory and set theory, list some open questions and speculate about a general characterization of mathematical intuition.


Brouwer, L. E. J., “Intuitionism and Formalism”, Bull. Am. Math Soc. 20 (1913): 81-96.

Brouwer, L. E. J., "Historical Background, Principles and Methods of Intuitionism", South African Journal of Science 49 (1952): 139-146.

Posy, C., "Intuitionism and Philosophy”, in The Oxford Handbook of the Philosophy of Mathematics. S. Shapiro, ed., Oxford University Press, 2004.

Meeting 5: Tuesday, June 16th. Double Session.

Session 1. 14h00

Frédéric Brechenmacher (École polytechnique), "Naturalness and effectiveness in Kronecker’s arithmetical theory of algebraic magnitudes"


The constructive nature of Kronecker’s 1882 Grundzüge einer arithmetischen theorie der algebraischen grössen has often been opposed to  Dedekind’s  structural approach to algebraic numbers. This talk aims at discussing the specificity of Kronecker’s theory in connection with more varied collective trends in the evolution of mathematics. The fist part of this talk shall investigate Kronecker’s ideal of "naturalness" in the framework of the development of Galois theory in the second half of the 19th century. The second part will discuss the role played by effective algorithms in Kronecker’s theory in connection with some specific practices developed in the framework of the theory of algebraic forms.


Brechenmacher, F., "Self-portraits with Évariste Galois (and the shadow of Camille Jordan)", Revue d'histoire des mathématiques 17 (2011): 271-369.

Brechenmacher, F., "La controverse de 1874 entre Camille Jordan et Leopold Kronecker", Revue d'histoire des mathématiques 13 (2007): 187-257.

Goldstein, C. & Schappacher, N., "A Book in Search of a Discipline (1801-1860)",  in Goldstein, C., and Schappacher, N., Schwermer, J., The Shaping of Arithmetics after C. F. Gauss's Disquisitiones Arithmeticae
Springer, 2007, 3-66.

Goldstein, C. & Schappacher, N., "Several Disciplines and a Book (1860-­1901)", in Goldstein, C., and Schappacher, N., Schwermer, J., The Shaping of Arithmetics after C. F. Gauss's Disquisitiones Arithmeticae,
Springer, 2007, 67-104.

Kronecker, L., "Grundzüge einer arithmetischen Theorie der algebraischen Grössen", Journal Fur Die Reine Und Angewandte Mathematik 92 (1882): 1-122.

Session 2. 16h15

Marco Panza (Université Paris 1, Pantheon-Sorbonne, IHPST; CNRS), "What makes Descartes' Geometrical Curves Geometrical and his Mechanical Curves Mechanical?"


I take Descartes's primary aim in La Géométrie to have been to promote a wide-ranging reform of (Euclid's) geometry, and to suggest a fresh foundation for it, one both consistent with, but also deeply innovative with respect to Euclid's. This resulted from an extension of Euclid's geometry, depending on an extension of its ontology, and made possible by an extended notion of (geometrical) construction, licensing constructions "by rule, compass, and reiteration". My purpose will be to briefly account for this extension and this new (albeit rooted in Euclid) notion of construction.


Bos, H., Redefining Geometrical Exactness, Springer, 2001.

Panza, M., "Rethinking  Geometrical Exactness", Historia Mathematica 38.1 (2011): 42-95. 

Meeting 6: Thursday, June 18th. Double Session.

Session 1. 14h00

Mark van Atten (SND [CNRS/Université Paris 4 Paris-Sorbonne]), "Kripke's Schema, transfinite proofs, and Troelstra's Paradox"


According to Brouwer, truth is experienced truth. Assumptions then have epistemic import: To assume that p is true is to assume that the subject has experienced its truth. This makes a difference for the way in which principles that involve an assumption can be justified. In this talk, I will discuss Kripke's Schema (KS) in this Brouwerian setting.

In the first part, I will give some examples of applications of KS in analysis, and go through an argument in its favour.

In the second part, I will try to meet some objections to KS that have been voiced by Kreisel, Veldman, and Vesley; in particular the objection that there is an incompatibility between (1) the idea, embodied in KS, that mathematical evidence comes in an ω-ordering, and (2) Brouwer's acceptance of transfinite (fully analysed) proofs.

In the third part, I argue that even though KS does not entail the theory of the Creating Subject (CS), in a Brouwerian setting objections to CS also undermine KS. The most prominent problem for CS is Troelstra's Paradox. As is well known, the construction of that paradox depends on the acceptability of a certain impredicativity; I argue that it moreover depends on Markov's Rule, and is therefore less threatening than it may seem.


Troelstra, A., Principles of Intuitionism (Lecture Notes in Mathematics, vol. 95). Berlin: Springer 1969 (section 16).

Dummett, M., Elements of Intuitionism, 2nd ed. Oxford: Oxford University Press 2000 (section 6.3).

van Atten, M., On Brouwer. Belmont: Wadsworth 2004 (chapter 5).

Sundholm, G. & M. van Atten,  "The proper explanation of intuitionistic logic: on Brouwer’s demonstration of the Bar Theorem", In M. van Atten, P. Boldini, M. Bourdeau, and G. Heinzmann (eds.), One Hundred Years of Intuitionism (1907–2007). The Cerisy Conference. Basel: Birkhäuser (pp. 60–77).

Session 2. 16h15

David McCarty (Indiana University-Bloomington), "Why is Intuitionism Constructive Mathematics?"


Intuitionism is mathematics only and mathematics entire. No weight of philosophy hangs permanently about its neck, dragging it under. There are no proprietary intuitionistic semantical rules, no special theories of meaning, no logical signs with arcane, intuitionistic connotations. For these are mere eyewash, nothing but mumbo-jumbo. Whatever justification or foundation may be required for this great subject comes from, and lives in the mathematics itself. Hence, it is with intuitionistic mathematics that one formulates and attempts to answer the questions, “What is a construction? To what extent, if any, is intuitionistic mathematics constructive?”


McCarty, D., "Antirealism and constructivism: Brouwer's weak counterexamples", Review of Symbolic Logic 6.1 (2013): 147-159.

McCarty, D., "Brouwer's weak counterexamples and testability: Further remarks", Review of Symbolic Logic 6.3 (2013): 513-523.

McCarty, D., "The new intuitionism" in van Atten et al. (eds.), One Hundred Years of Intuitionism, pp. 37-49, Birkhäuser, 2008.

Meeting 7: Tuesday, June 23rd, 16h00

Nathan Sidoli (Waseda University), "Constructions and Problems in Euclid's Elements"


There has been considerable recent work by logicians and philosophers of mathematics on the constructive aspects of Euclidean geometry, and the deductive force involved in reasoning with diagrams. In this talk, I present a reading of Euclid's Elements that shows that there is a difference in the way that constructions are used in theorems and in problems. I will show how Euclid presents his problems as series of well-formed routines, and subroutines, that allow geometric objects to be created through intuitive constructive processes that rely only on the first three postulates. By making a close reading of Elements III.1 and II.11, I will show that (a) problems are not meant to present a practical method of drawing with a straight-edge and compass, but rather demonstrate the feasibility of constructive processes built up from the postulates, and (b) that constructions in the theorems do not function in this way, but allow of a wider possibility of constructive assumptions, whose motivation is based on the needs of proof. Hence, the development of the problems must be understood as an independent project from the role of constructions in theorems.


Beeson, M., "Constructive geometry", in Arai, T., Brendle, J., Kikyo, H., Chong, C.T., Downey, R., Feng, Q., Ono, H. (eds.), Proceedings of the 10th Asian Logic Conference. World Scientific, Hackensack, New Jersey, pp. 19–84, 2010.

Catton, P. & C. Montelle, "To diagram, to demonstrate: To do, to see and to judge in Greek geometry", Philosophia Mathematica 20 (2012): 25-57.

Mäenpää, P. & J. von Plato, "The logic of Euclidean construction procedures", Acta Philosophica
49 (1990): 275–293.

Manders, K., "The Euclidean diagram (1995)", in Mancosu, P. (ed.), The Philosophy of Mathematical
. Oxford University Press, Oxford, pp. 80–133, 2008.

Netz, R., "Proclus' division of the mathematical propositions into parts: How and why was it formulated?", Classical Quarterly 49 (1999): 282-303.

Pambuccian, V., "Axiomatizing geometric constructions", Journal of Applied Logic 6 (2008): 24–46.

Panza, M., "The twofold role of diagrams in Euclid’s plane geometry", Synthese 186 (2012): 55–102.

Sidoli, N. & K. Saito, "The role of geometrical construction in Theodosius' Spherics", Archive for the History of the Exact Sciences 63 (2009): 581-609.

Meeting 8: Thursday, June 25th, 16h00

Orna Harari (Tel Aviv University), "Geometrical Construction: Greek Philosophical Perspectives"


The use of geometrical constructions in Greek mathematical proofs attracted the attention of several Greek philosophers. Their reactions to this practice vary from dismissal and underestimation of their importance to an acknowledgement of their indispensability for establishing geometrical theorems. In this talk, I discuss the philosophical motivations behind these reactions. Specifically, I try to explain why Aristotle ignores geometrical constructions in his account of demonstrative knowledge and Proclus sets this topic as one of the goals of his philosophy of mathematics. I show that these two approaches do not arise from an attempt to understand the geometers’ use of constructions but from philosophical considerations, such as the status of relational attributes, the ontological status of mathematical objects, the status of mathematics as a science, the nature of the human intellect, and the relationship between philosophy and the other sciences.


Knorr, W., "Constructions as Existence Proofs in Ancient Geometry", Ancient Philosophy 3 (1983), 125-128.

Mueller, I., "On the Notion of Mathematical Starting Point in Plato, Aristotle, and Euclid", in Bowen, A.C. (ed), Science and Philosophy in Classical Greece, New York 1991.

Mueller, I., Proclus, A commentary on the First Book of Euclid's Elements, Princeton 1992, foreword by Mueller, ix-xxxi.


♦ Directors: Pr. Michael Detlefsen (University of Notre Dame) and Pr. Jean-Jacques Szczeciniarz (Université de Paris 7-Diderot)