zh-tw:logic [2012 Formosan Summer School on Logic, Language, and Computation (FLOLAC '12)]


Lecturer: 柯向上 Hsiang-Shang Ko

Introduction to formal logic, with a bias towards proof theory. Highlights of this course:

  • the use of formal languages to represent reasoning patterns;
  • reasoning in the meta-language about the object language (especially by induction);
  • the intimate connection between logic and computation.

Outline & slides

    • Formal languages of propositional & first-order logic
    • The Brouwer–Heyting–Kolmogorov interpretation
    • Natural deduction
    • Heyting arithmetic
    • Syntactic consistency and completeness
    • Classical semantics of propositional & first-order logic
    • Soundness and semantic completeness
    • Gödel–Gentzen negative translation (if time permits)
    • Simply typed λ-calculus with constants
    • Proof normalisation
    • Dependent types