Anders Lundstedt: Imprecise thoughts entertained in mathematical practice and the special case of unprovability by straightforward induction
Time: Wed 2022-03-23 10.00 - 12.00
Location: Kräftriket, House 5, Room 31
Lecturer: Anders Lundstedt (Stockholm University, Dept of Philosophy)
Mathematical definitions, results and proofs are almost always precisely formulated (modulo details left for readers). On the other hand, when mathematicians talk or think about definitions, results and proofs, their formulations are not always precise.
(1) Mathematicians sometimes entertain thoughts to the effect that a certain proof uses this or that method—while not always having a precise and sensible meaning in mind for ‘this proof uses this or that method’.
(2) Mathematicians sometimes talk about new proofs of already established results—while not always being precise in what sensible sense the new proof indeed ought to qualify as new.
(3) Mathematicians sometimes claim that this or that fact's provability requires a certain “idea”—for example, a lemma or a certain kind of construction.
(4) Mathematicians sometimes use the predicates ‘natural’ and ‘unnatural’ in intuitive but imprecise ways—as in, for example, something like “that is a very unnatural proof”.
(5) In addition to examples (1)–(4), I have observed some hostility among some mathematicians towards imprecisely phrased questions regarding mathematical matters. Perhaps this is just me being biased due to my frustration with MathOverflow closing some more or less imprecise questions that I from time to time find interesting and would like to see discussed.
This talk should be quite accessible. The plan is as follows:
- to briefly tell the story of how I first got interested in the problem of making precise and sensible sense of imprecise things thoughts entertained in mathematical practice;
- give some real-world examples falling under one or more of (1)–(5) above, and for each briefly discuss whether it would be worth to try to find a precise and sensible formulation; and
- in preparation for my talk at next week's seminar—and in particular for its connection with (3)–(5) above—conclude with an introduction to my work on non-straightforward induction proofs, going into some technical details if time permits.
(“Non-straightforward” induction proofs are more often called something like “proofs by generalizing the statement to prove”, but as Eric Johannesson and I have shown, there are cases where “induction on the statement itself” provably does not work, while—perhaps surprisingly—an induction proof of a less general statement, or of a weaker or incomparable statement, succeeds and gives the desired statement as an immediate consequence.)
- Hetzl, Stefan, and Tin Lok Wong (2018): Some observations on the logical foundations of inductive theorem proving. In: Logical Methods in Computer Science 13(4), pp. 1–26. (Corrected version of paper originally published Nov 16, 2017.)
My research page has some material, but it is very outdated. Hopefully very soon I will upload at least some of the following:
- Lundstedt, Anders (2022): Non-straightforward induction proofs and the comparative strength of inductive solutions. Revised manuscript for the presentation at the online seminar of the Computational Logic group of the Institute of Discrete Mathematics and Geometry, TU Wien, May 12, 2021.
- Lundstedt, Anders (2022): Some non-inductive formulas. Manuscript in preparation.
- Lundstedt, Anders, and Eric Johannesson (2022): Comparing inductive solutions. Manuscript in preparation.