PhilMath Intersem 4.2013
This year will be the fourth meeting of the PhilMath Intersem, PhilMath Intersem 4.
Theme
The theme of this year’s seminar is “Indirect Proof.”
Place(s)
All meetings except the eighth (June 21st) will be in Paris. The eighth meeting will be at the University of Lorraine-Nancy. That meeting is a double session and will begin at 14h00.
Paris Place
The room for all the Paris meetings will be the salle Klimt (366A) in the Condorcet building on the Rive Gauche campus of the University of Paris 7-Diderot (P7).
Public access to the Condorcet building is at 4 rue Elsa Morante, which is on the A side of the building.
Nancy Place
The room for the Nancy meeting will be the salle Internationale on the third floor (as the French number floors) of the MSH building on the University of Lorraine-Nancy campus.
This is on the same floor as the Archives Henri Poincarè.
The address is: 91, av. de la Libération
Here’s a map to help you get from the main Nancy train station to the MSH building.
Useful links
Rive Gauche campus of P7 (for those who may know how to fly)
Condorcet Building on Rive Gauche campus
Archives Henri Poincaré at the University of Lorraine
Schedule
Meeting 1. June 4, 16h00
Vincenzo De Risi, Research Group Director, Max Planck Institute for the History of Science, Berlin
“What does it mean to (indirectly) prove the Parallel Postulate? Some developments in mathematical epistemology from Euclid to Lambert”
Abstract
In this talk I discuss some attempts of an indirect proof of the Parallel Postulate, from ancient times to the 18th century. As the question “What is a geometrical principle?” receives different answers in different centuries, we see that the act of denying the Parallel Postulate at the beginning of the various proofs has different outcomes as well. Thus, even though we find a steady development in the formal aspects of these attempts, the meaning of them is widely different. The history of the changing mathematical epistemology behind the Parallel Postulate may account for the acceptance of non-Euclidean geometries in the 19th century, as well as for the development of new strategies of indirect proofs.
Reading
Al-Nayrizi, The Commentary on the first book of Euclid’s Elements (English translation by A. Lo Bello)
Harari, O. “Proclus’ Account of Explanatory Demonstrations in Mathematics and its Context”, Archiv für Geschichte der Philosophie 90 (2008): 137-164
Mancosu, P. “On the Status of Proofs by Contradiction in the Seventeenth Century”, Synthese 88 (1991): 15-41
Mueller, I. “On the Notion of a Mathematical Starting Point in Plato, Aristotle, and Euclid”, in A.C. Bowen (ed.), Science and Philosophy in Classical Greece, London and New York, Garland1991, pp. 59-97
Proclus, Commentary on Euclid’s Elements (esp. the section on the Parallel Postulate)
Saccheri, G. Euclides Vindicatus (English translation by Halsted)
Meeting 2. June 6, 16h00
Stephen Read, Arché Research Centre for Logic, Language, Metaphysics and Epistemology, University of St Andrews
“Indirect Proof in Medieval Logic”
Abstract
Aristotle’s own method of establishing the validity of his categorical syllogisms used conversions and the dictum de omni et nullo. But these proof methods did not suffice for all the valid syllogisms, and those others he established by reductio per impossibile. This method of indirect proof was therefore familiar to medieval logicians after recovery of the Prior Analytics during the twelfth century. They also drew from Aristotle the use of the dialectical syllogism in the Topics, which led to the development of logical exercises called “Obligations”. In these, an Opponent attempts to force the Respondent to concede a contradiction from a false hypothesis according to certain prescribed rules. Finally, there is a use of indirect proof in the popular medieval genre of Sophismata, arguing for both a thesis and anti-thesis, subsequently diagnosing the fallacy in one or other argument.
Reading
Simo Knuuttila, “Modality’, especially §2: Extensional Modalities in Obligations Logic and Indirect Proofs”, in The Oxford Handbook of Medieval Philosophy, OUP 2012, ed. J. Marenbon, 315-21.
Chris Martin, “Obligations and Liars”, in Medieval Formal Logic, ed. Mikko Yrjönsuuri, Kluwer 2001, 63-94. (Originally published in Sophisms in Medieval Logic and Grammar, ed. S. Read, Kluwer 1993, 357-81.)
Meeting 3. June 11, 16h00
Fabio Acerbi, CNRS, UMR 8560
“Proofs by Consequentia Mirabilis in Greek Mathematical Works”
Abstract
The paper discusses the alleged applications of consequentia mirabilis in Greek mathematical works. The discussion is further enlarged to a critical assessment of the methodology applied by many interpreters in seeking for particular logical rules at work in ancient mathematical texts, in particular their acceptance of the modern conception of logical rules as tautologies.
Reading
Bellissima F., Pagli P., Consequentia mirabilis. Una regola logica tra matematica e filosofia. Firenze, Leo S. Olschki, 1996. [This book contains a full collection of sources (restricted to Ancient and Early modern writings) on consequentia mirabilis.]
Castagnoli L., “Self-Bracketing Pyrrhonism”, Oxford Studies in Ancient Philosophy 18 (2000): 263–328.
Castagnoli L., Ancient Self-Refutation: The Logic and History of the Self-Refutation Argument from Democritus to Augustine. Cambridge: Cambridge University Press, 2010
Clavius Ch., Commentaria in Euclidis Elementa Geometrica, in Opera Mathematica. Moguntiae, 1611 (available online at www.e-rara.ch).
Vailati G., “A proposito di un passo del Teeteto e di una dimostrazione di Euclide”, Rivista di Filosofia e scienze affini 6, 5–15 (French transl. with additions: Sur une classe remarquable de raisonnements par réduction à l’absurde. Revue de Métaphysique et de Morale 12 (1904), 799–809).
Meeting 4. June 13, 16h00
Catarina Dutilh-Novaes, Department of Theoretical Philosophy, University of Groningen
“Indirect proof in the Prior Analytics from a dialogical perspective”
Abstract
It is well known that indirect proofs, reductio proofs in particular, pose interesting philosophical questions. What does it mean to assert something with the precise goal of then showing it to be false, i.e. because it leads to absurd conclusions? Why assert it in the first place? What kind of speech act is that? Moreover, the mathematics education literature has numerous studies showing how hard it is for students to truly comprehend the idea of reductio proofs, which indicates the cognitive complexity of these constructions.
Historically, the emergence of the technique of indirect proofs arguably marks the very birth of the deductive method (both in mathematics and in logic), as it appears to be a significant departure from more ‘mundane’ forms of argumentation. So it is perhaps not surprising that the first fully-fledged logical text in history, the Prior Analytics, offers a sophisticated account of indirect proofs.
In my talk, I take as a starting point a dialogical conceptualization of deductive proofs and argue that the theory of syllogistic in the Prior Analytics is best understood from a dialogical perspective. I illustrate this claim by analyzing Aristotle’s conception of a reductio proof in the Prior Analytics from this point of view. More generally, I argue that many of the philosophical and cognitive difficulties surrounding reductio proofs are disspelled once one adopts a dialogical perspective.
Reading
Kapp, Ernest. “Syllogistic.” In Articles on Aristotle. Vol. 1 Science, edited by Barnes, Jonathan, Schofield, Malcolm and Sorabji, Richard. 35-49. London: Duckworth, 1975
Hodges, Wilfrid, “Indirect proofs and proofs from assumption”
C. Dutilh Novaes, “A dialogical conception of indirect proofs”. Blog post
C. Dutilh Novaes, “Indirect proofs in the Prior Analytics”. Blog post
Meeting 5. June 14, 16h00
David Rabouin, CNRS, SPHERE, University of Paris 7-Diderot
“What do indirect proofs have to tell us about mathematical objects?”
Abstract
Indirect proofs are very widespread in Ancient Greek Mathematics. Almost one quarter of Euclid’s propositions in the Elements use for example, in one form or another, reductio arguments.
These proofs have attracted a lot of attention regarding their logical structure, but not so much concerning what they have to tell us
about mathematical objects. My aim is to address this issue.
Among reductio proofs, some have a very noticeable form: they ask us
to deny a characteristic property of familiar mathematical objects (such as
parallel lines being said to intersect or distinct circles presented at once as
cotangent and concentric).
What are these propositions referring to? “True” parallel lines and circles?
If not, what are these “objects”?
Moreover, in the case of geometry, these proofs rely on diagrams which “represent” impossible states of affair. How can we “represent” something impossible?
In the pars destruens of my talk, I would like to show that many philosophical claims about mathematical objects and geometrical diagrams are not able to provide an answer to these questions.
In the pars construens, I will try to sketch a possible account of these situations by using the notion of “material anchoring” of inferences and a Putnamian approach to reference.
Reading
Gardies, J.-L., Le raisonnement par l’absurde, Paris: P.U.F., 1991
Manders, K., 2008, “The Euclidean diagram” in P. Mancosu (Ed.), The Philosophy of Mathematical Practice, Oxford: Oxford University Press, 80-133 (especially pp. 109-118 on reductio).
Netz, R., 2003, The Shaping of Deduction in Greek Mathematics : A Study in Cognitive History, Cambridge: Cambridge University Press.
Proclus, 1992, A commentary on the First Book of Euclid’s Elements, Princeton, Princeton University Press, transl. G.R. Morrow, preface by I. Mueller.
Vitrac, B., Les démonstrations par l’absurde dans les Éléments d’Euclide :
inventaire, formulation, usages
Meeting 6. June 18, 14h00 (earlier starting time, double session)
Paul Rusnock, Department of Philosophy, University of Ottawa
Jan Sebestik, Czech Academy of Science
“Bolzano on Indirect Proofs”
Abstract
Bolzano calls indirect or apagogical proofs those where, « instead of the proposition to be proved we contemplate its contradictory opposite, and show that from this, along with certain other already proved truths, follows a conclusion that is obviously false« (Mathematical Method, §16). He is suspicious about such proofs because they deduce the conclusion from a false premise. He does not deny that they are apt to reach certainty of a proposition, but he asks whether they can also provide its objective ground, which is the ultimate goal of the presentation of a science. They can do it, but as they proceed by a detour (Umweg), the objective ground never appears as clearly as in direct proofs. Bolzano believes (and tries to prove) that, on one hand, through a simplification, one can transform them into direct proofs, but on the other hand, they are useful because they suggest themselves more readily and are more easily expressed. This is why Bolzano will use them “here and there” in his Theory of science, Theory of magnitude and elsewhere.
Reading
Bolzano, B., Wissenschaftslehre, I-IV (on apagogical proofs: IV, § 530) Sulzbach, 1837, Engl. transl. by P. Rusnock and R. George, forthcoming, Oxford University Press.
Bolzano, B., Einleitung in die Grössenlehre und Erste Begriffe der allgemeinen Grössenlehre (Introduction into the Theory of Magnitudes and First concepts of the general Theory of Magnitudes), Bernard-Bolzano Gesamtausgabe, II A 7, Stuttgart-Bad Cannstatt, Fromann-Holzboog1976; Engl. transl. of the chapter On the mathematical method, by P. Rusnock and R. George, Amsterdam-New York, Rodopi, 2004,; Ital. transl. 1966; French transl. Paris, Vrin, 2008).
Berka K., “Zur Auffassung des apagogischen Beweises bei B. Bolzano”, Acta hist. rerum nat. necnon techn., Prague, 1981, special issue 16, 30-42.
Hafner, J., “Bolzano’s criticism of indirect proofs”, Revue d‘histoire des sciences 52 (1999), n° 3-4: 385-398.
Löwenheim L., “On making indirect proofs direct”, transl. by W. V. Quine, Scripta mathematica 12 (New York 1946), 125-39.
Meeting 7: June 20, 16h00
Greg Restall, Department of Philosophy, University of Melbourne
“Indirect Proofs and Proof Structures for Classical Logic”
Abstract
In this talk, I will show how contemporary proof structures for classical logic (derived both from early work due to William and Martha Kneale; Carnap; and Shoesmith and Smiley, and then in contemporary work on proof nets from Girard and his collaborators) can be understood and motivated by way of considerations concerning indirect proof. I will introduce this minority tradition in proof theory to a broader audience, and show how seemingly odd, esoteric and unnatural features of these proof structures actually have natural interpretations, and that these structures can be seen to undergird indirect proof.
Reading
William and Martha Kneale (1962) The Development of Logic, Clarendon Press. See especially Chapter IX, Section 3.
Roberto Di Cosmo and Dale Miller (2010) “Linear Logic,” Stanford Encyclopedia of Philosophy, Section 3.
Greg Restall (2005) “Multiple Conclusions,” in Logic, Methodology and Philosophy of Science: Proceedings of the Twelfth International Congress, edited by Petr Hajek, Luis Valdes-Villanueva and Dag Westerstahl, Kings’ College Publications, 2005, 189–205.
D. J. Shoesmith and T. J. Smiley (1978) Multiple-Conclusion Logic, Cambridge University Press, Chapters 2, 3.
Meeting 8. June 21: 14h00 Nancy (earlier starting time, double session)
Greg Restall, Department of Philosophy, University of Melbourne
“Warrant in Indirect Proofs”
Abstract
In this talk, I will show how contemporary developments in term assignment systems for classical sequent calculus and natural deduction can be given an interpretation in terms of the dual notions of warrant for and warrant against a claim in the same sort of way that the traditional lambda calculus can be interpreted simply as manipulating warrant for. We will attempt to explain all of this clearly and succinctly, and to apply it to specific examples of reasoning by indirect proof.
Reading
Pierre-Louis Curien and Hugo Herbelin (2000) “The Duality of Computation” in Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP): 233–243.
Jean-Yves Girard (1987) “Linear Logic,” Theoretical Computer Science, London Mathematical 50:1, pp. 1-102.
John Mumma, Department of Philosophy, California Sate University-San Bernardino
“The indirect proof approach to parallelism”
Abstract
In Hilbert’s Foundations of Geometry parallelism in the Euclidean plane is understood as a relation between lines of infinite extent. Pairs of such lines either intersect or are parallel. If in contrast a more complex conception of Euclidean lines is presumed, whereby they are bounded objects that can be extended indefinitely, a more complex conception of parallelism is (arguably) required. On this conception, parallelism is not something that can be directly asserted or proved of a configuration; establishing it requires an indirect proof. I examine how this conception has and can be realized formally by considering (Von Plato, 1995) and (Avigad et al. 2009). I then comment on the extent to which the conception can be said to be present in Euclid’s Elements and Saccheri’s Euclides Vindicatus.
Reading
J. Avigad, E. Dean, and J. Mumma (2009). “A formal system for Euclid’s Elements,” Review of Symbolic Logic, 2:700–768.
Euclid, Elements, Bk. I, Prop 27.
J. Von Plato (1995). “The axioms of constructive geometry,” Annals of Pure and Applied Logic. 76:169-200.
Meeting 9: June 25, 16h00
Göran Sundholm, Institute of Philosophy, University of Leiden
“Definition of functions by undecided separation of cases”
Abstract
A common use of non-constructive reasoning – “indirect demonstration” – in mathematics is to give a definition by asking a non-decidable question about a function, for instance a choice function w.r.t. a certain set. For the rest, all the logic used in the demonstration might be as constructive as can be, but the demonstrated theorem will nevertheless be non-constructive. Examples of this phenomenon are the Theorem of Bolzano-Weierstraß and Zorn’s Lemma.
Classically, where the Law of Excluded Middle and unlimited comprehension are freely available, the characteristic function of a set is readily obtained by means of an undecided separation of cases, whence sets may be represented by their characteristic functions, and vice versa, and functions by their graphs. Constructively, the existence of functions is much less troublesome than the existence of sets, hence the Axiom of Exponentiation is considerably weaker than Power Set and Comprehension.
The characteristic function of Kleene’s non-recursive, recursively enumerable set K, Kripke’s formally similar non-recursive function that however is “computable” via the Brouwer-Kreisel-Myhill theory of the creative subject, and Kalmár’s alleged “counterexample” to Church’s Thesis will be considered and compared from a constructive position, using Martin-Löf’s Constructive Type Theory for my logic. If time permits, Kreisel’s elimination of Non-Constructive Dilemma with respect to “∀z A(z)” assumptions with a decidable matrix A, in arithmetical demonstrations of theorems of the form “∀x∃y B(x,y)”, again with decidable matrix B.
Reading
• On Kripke’s Schema, Brouwer’s Theory of the Creative Subject, and Church’s thesis
Mark van Atten, ‘The foundations of mathematics as a study of life: an effective but non-recursive function’, Progress in Theoretical Physics, n° 173 (2008): 38-47
• On Kalmár’s “counterexample”
Lászlo Kalmár, 1959, ‘An Argument Against the Plausibility of Church’s Thesis’, in: A. Heyting ( ed.), Constructivity in Mathematics, North-Holland, Amsterdam (1959), 72-80
• On the elimination of non-constructive dilemma
Kreisel, G. “Mathematical Significance of Consistency Proofs”, JSL 23(1958): 155-182 (see esp 169-170
• On constructive dilemma and the definition of functions by separation of cases
Per Martin-Löf, Intuitionistic Type Theory, Bibliopolis, Naples 1984, especially at pp. 55-58
Nordström, Bengt, K. Petterson and J. Smith, Programming in Martin-Löf’s Type Theory, Clarendon, Oxford, 1990, esp. 176-180 [On constructive dilemma and the definition of functions by separation of cases]
Meeting 10. June 27, 16h00
Victor Pambuccian, School of Mathematical and Natural Science, Arizona State University
“Forms of indirect proof in elementary geometries”
Abstract
We will focus on three forms of “indirectness”: (1) proofs that proceed via the contrapositive, asking in a very specific case, the Steiner-Lehmus theorem, which states that a triangle with two congruent internal angle bisectors must be isosceles, if there is a direct proof, defining in precise terms, using the sequent calculus, what is meant by a direct proof. The question regarding a direct proof goes back to 1852, when it was raised by J.J. Sylvester; (2) proofs that require representation theorems that tell us that every model of the theory in question is isomorphic to a certain algebraic structure, where no actual formal proof is known; (3) proofs in which a certain axiom has to be used more than once.
Reading
Negri, Sara; von Plato, Jan Structural proof theory, Appendix C by Aarne Ranta, Cambridge University Press, Cambridge, 2001
Negri, Sara; von Plato, Jan “Cut elimination in the presence of axioms”, Bull. Symbolic Logic 4 (4) (1998): 418-435
Pambuccian, Victor “Early examples of resource-consciousness”, Studia Logica 77 (1) (2004): 81-86