• Overview
• Details
• Exercises

First-order logic (FOL) extends propositional logic with quantifiers and predicates over a domain of discourse. It underpins mathematical logic, formal verification, and knowledge representation.

• Syntax: terms, formulas, free vs bound variables
• Semantics: structures/interpretations, satisfaction, validity
• Quantifiers: ∀ (universal), ∃ (existential); prenex normal form
• Inference: natural deduction, sequent calculus, resolution
• Limits: completeness (Gödel), compactness, Löwenheim–Skolem

1. Translate English statements into FOL with a chosen signature.
2. Convert a formula to prenex and Skolem normal forms.
3. Prove a simple theorem using natural deduction rules.