Outline
Meeting 12: December 6
Euclidean diagrammatic reasoning, following the slides here.
Meeting 11: November 20
Modularity
- mathematics from a design standpoint
- modularity in complex systems
- modularity in computer science
- modularity in mathematics
- case studies
Meeting 10: November 13
Arana, "On the depth of Szemeredi's theorem"
- overview of Szemeredi's theorem
- views of depth: genetic, evidentialist, consequentialist, "cosmological"
Detlefsen, "Duality, epistemic efficiency, and consistency"
- examples: projective geometry, Boolean algebras, category theory
- different senses of dualization
- the epistemic calculus
- self-dual vs. non-self-dual axiomatizations
Meeting 9: November 6
Hamami, "Mathematical rigor, proof gap, and the validity of mathematical inference"
- the notion of a gapping
- Prawitz' account of grounds and operations
- Kitcher on a "mathematical practice"
- Intra vs. inter-practice gaps
Interactive theorem prover languages
- components of a proof language
- Wiedijk, "the mathematical vernacular"
- SSReflect
Meeting 8: October 30
Manders, "Expressive means and mathematical understanding"
- conceptual recasting
- merelification
- linguistic restriction, modes
- Euclidean devices to "suppress and retain responsiveness"
- Descartes
Hardalupas, "When is a proof not a proof?"
- traditional proofs vs. computer proofs, accounting for the differences
- why do mathematicians prove theorems?
- proof as narrative
- historical narrative vs. literary narrative
Meeting 7: October 16
Dirichlet's theorem, following these slides.
Meeting 6: October 9
Simon, "Architecture of Complexity"
- recap from last week
- near decomposibility
- descriptions of complex systems, understandability
- state descriptions vs. process descriptions
- conclusions
Parnas, "On the criterion..."
- two modularizations
- differences
- conclusions
Structure and Interpretation of Computer Programs
- building abstractions with procedures (primitive combinations, means of combination, means of abstraction)
- local names
- higher-order procedures
- building abstractions with data
- abstraction barriers, multiple representations (type tags), generic operations, coercions
- modularity, objects, and state
- state vs. streams
Meeting 5: October 2
Birner and Ward
- open propositions
- preposing, inversion, gapping, etc.
- the methodology of linguistics
Mathematical texts
- excerpt from Hatcher, Algebraic Topology
- excerpt from Hardy and Wright, Introduction to the Theory of Numbers
Modularity
- designed systems vs. natural systems
- hierarchy vs. modularity
- benefits
Simon, "Architecture of Complexity"
Meeting 4: September 25
Kaplan on "ouch" and "oops"
- recap of last week
- "ouch" vs. "oops," subjective vs. objective expressives
- "and" and "but," distinctions between descriptive content, expressive content, and pragmatics
- translation, and the distinction between linguistic conventions and social conventions
- conclusions
Birner and Ward
- information structure
- preposing, left-dislocation, postposing, and right-dislocation
Meeting 3: September 18
Interactive theorem proving
- formal sytems: expressive strength rather than logical strength
- varieties of proof languages
- proof languages and programming languages
Moving beyond the "standard" model of proof
- coarser steps, real-world justifications
- active language: apply, calculate, construct, ...
- non-inferential content: examples and special cases, motivation, key ideas
- subtleties of communication: word order, linguistic variation
Q: Does proof language change over time? Across cultures?
Kaplan on "ouch" and "oops"
- the formalist tradition vs. meaning as use
- partial reconciliations: Grice (conventional meaning vs. pragmatics), Searle (logic of speech acts)
- semantic information (descriptive vs. expressive content)
- logical validity and entailment in this more general context
Meeting 2: September 11
Mathematical method and proof
- traditional views of mathematical knowledge
- more robust views: theorems, definitions, proofs, questions, concepts, methods, heuristics, ...
- products of sums of squares: evaluating proofs
- conclusions
Interactive theorem proving, following this survey: pdf.
Meeting 1: September 4
Course mechanics
Ideas, motivation, and background stories
- Formalizing the PNT; the structure of mathematical knowledge, and normative assessments in mathematcs
- The history of Dirichlet's theorem, modularity, and refactoring
- The design of an interactive theorem prover, and artificial languages
Goals / questions
- Consider informal mathematics as a designed language. What are the design constraints? What are the mechanisms by which it attains its goals?
- Consider formal proof languages. Can we develop a good design theory? Can we use insights from the design of programming languages? Can we use semantic approaches?
- What does this have to tell us about mathematical knowledge, ontology, and the history of mathematics?