# Elementary Logic

- Lecturer: 柯向上 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

TBA