基礎邏輯 (Elementary Logic)

• 講者: 柯向上 Hsiang-Shang Ko

Focusing on propositional logic, leaving quantification to MLTT. It would be easier to have some intuition from FP (e.g., pattern matching and induction); also it is strongly desirable to let the students see some concrete examples of proofs (beforehand, probably also in FP).

Outline​

• Intuitionistic logic (1 unit)
  • Propositional formulas
  • Follow-your-nose proofs
  • Natural deduction
  • Reflection on classical reasoning principles
• Classical logic (1 unit)
  • Two-value semantics
  • Consistency
  • Soundness and (in-)completeness
  • Double-negation translation (Glivenko’s Theorem)

Course Materials

• slides 1
• slides 2
• 上課塗鴉版投影片