PHIL 2505 Contentualness & Formalism (Spring 2026)
Instructor: Doug Blue
Email: doug.blue[at]pitt.edu
Meetings: Tuesdays 10am-12:30pm in CL 1008B
Description
David Hilbert once described "the question of relations between contentualness (Inhaltlichkeit) and formalism in mathematics and logic" as among the most difficult epistemological problems with scientific significance. This seminar will take up that question directly.
Our central text will be Juliette Kennedy’s Gödel, Tarski and the Lure of Natural Language: Logical Entanglement, Formalism Freeness, through which we will explore the epistemological advantages of formalization in mathematics and the phenomenon of "formalism freeness." Along the way, we will consider questions such as:
- How does formalization contribute to knowledge acquisition?
- What is the meaning of mathematical language?
- What counts as a natural formal theory?
- To what extent are formal systems adequate models of mathematical practice?
We will reflect on the broader implications of these issues for the philosophy of mathematical practice, traditional philosophy of mathematics, and linguistic philosophy, both ideal and ordinary.
Course structure
The course will consist of four units.
- Rigor
- The relation of mathematical logic to mathematics
- Intension and interpretation
- Formalism freeness
Requirements
Auditors and participants taking the course for credit may be asked to present material.
Participants taking the course for credit are expected to write a term paper.
References
Under construction.
Books
- Baldwin, Model Theory and the Philosophy of Mathematical Practice
- Burgess, Rigor and Structure
- Kennedy, Gödel, Tarski and the Lure of Natural Language: Logical Entanglement, Formalism Freeness
Hilbert and the contentual
- Blanchette, The Frege-Hilbert controversy.
- Hilbert, On the infinite.
- Hilbert, Axiomatic thinking.
- Mancosu, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s.
Rigor
- Avigad, Understanding proofs.
- Avigad, Understanding, formal verification, and the philosophy of mathematics.
- Avigad, The mechanization of mathematics.
- Avigad, Relibability of mathematical inference.
- Avigad, Mathematics and the formal turn.
- Azzouni, How and why mathematics is unique as social practice.
- Azzouni, Why do informal proofs conform to formal norms?
- Azzouni, Does reason evolve? (Does the reasoning in mathematics evolve?)
- Azzouni, The algorithmic-device view of informal rigorous mathematical proof.
- Burgess & De Toffoli, What is mathematical rigor?
- De Toffoli, Reconciling rigor and intuition.
- De Toffoli, Proofs for a price: Tomorrow's ultra-rigorous mathematical culture.
- Feferman, And so on...: Reasoning with infinite diagrams.
- Granville, Proof in the time of machine.
- Hamami, Mathematical rigor and proof.
- Harris, Automation compels mathematicians to reflect on our values.
- Larvor, How to think about informal proofs.
- Larvor, Why the naive derivation recipe model cannot explain how mathematicians' proofs secure mathematical knowledge.
- Paseau, What's the point of complete rigour?
- Rav, Why do we prove theorems?
- Rav, A critique of a formalist-mechanist version of the justification of arguments in mathematicians' proof practices.
- Tanswell, A problem with the dependence of informal proofs on formal proofs.
- Tanswell, Mathematical Rigour and Informal Proof.
- Thurston, On proof and progress in mathematics
- Wagner, Mathematical consensus: a research program.
- Weatherall & Wolfson, Correctness, artificial intelligence, and the epistemic value of mathematical proof.
- Wu et al., Autoformalization with large language models.
Mathematical logic and practice
- Baker, Non-deductive methods in mathematics.
- Cheng, Mathematics, morally.
- De Toffoli and Mancosu, Philosophy of mathematical practice.
- Hofweber, Formal tools and the philosophy of mathematics
- Kreisel, Mathematical logic: what has it done for the philosophy of mathematics?
- Kreisel, Mathematical logic: Tool and object lesson for science
- Macintyre, The mathematical significance of proof theory.
- Polya, Mathematics and Plausible Reasoning
- Post, Absolutely unsolvable problems and relatively undecidable
propositions–account of an anticipation.
Formal mathematics & verification
- Avigad, Is mathematics obsolete?.
- Buzzard, Mathematical reasoning and the computer.
- Commelin, Abstract formalities (video).
- De Millo, Lipton, and Perlis. Social processes and
proofs of theorems and programs.
- Hales, Big conjectures (video)
- Kontorovich, The shape of mathematics to come.
- Macbeth, Algorithm and abstraction in formal mathematics.
- Mackenzie, Mechanizing proof.
- Wayne, Three ways formally verified code can go wrong.
Logic in mathematics
- Kaye, Review of Craig Smorynski, Logical Number Theory I, An Introduction.
- Poonen, Barry Mazur's work relating logic and arithmetic geometry.
- Poonen, Undecidability in number theory.
- Poonen, Undecidable problems: a sampler.
Logic as modeling
- Barwise, Noun Phrases, Generalized Quantifiers and Anaphora
- Cook, Logic-as-modeling: a new perspective on formalization, PhD thesis
- Kripke, The question of logic.
Intension and interpretation
- Feferman, Arithmetization of metamathematics in a general setting.
- Lindstrom, Aspects of incompleteness.
Natural theories and linearity