Metamathematics Seminar

This is like TTFV, but for the more theory-minded people.

Plan

• From ΠΣ to inductive datatypes
• Primitive Agda
• Intuitionistic Logics
  • Propositional
  • Simply typed λ-calculus
  • First-order
    • Predicate
  • λP₁
  • Second-order
    • Propositional
    • Predicate
  • HM and λ2
  • Curry’s paradox
  • High-order
  • λP
• Axioms and Axiom schemes
• ? Finite Sets
• ? Models
• Peano Arithmetic and Agda
• Constructive Set Theory and Agda
  • Russell’ paradox
  • Curry’s paradox
  • Universal set
• The law of the excluded middle, extrapolation to infinite sets
  • ZF
  • NBG
  • Axiom of choice, Zorn’s lemma, Zermelo’s theorem
• Ordinals
  • Up to ω
  • Constructive
  • Classical
  • Arithmetic
  • Burali-Forti paradox
• Cardinals
  • Constructive
  • Classical
  • Arithmetic
• High-order Type Theories
  • Pure Type Systems
  • Martin-Löf Type Theory and variants
    • Identity types
    • ΠΣW
    • ΠΣμ
  • “Axiom of choice” theorem
  • Girard’s/Hurken’s paradox