FirstOrderLogic

First-order logic extends propositional logic with quantifiers, following Popper’s theory of quantification: substitution as a structural operation, with the quantifiers themselves defined from it rather than taken as new primitive axioms.

Rather than reformalizing terms, structures, and satisfaction, this chapter builds directly on Mathlib’s own model theory.

• Formula
  • Difficulty: hard (2 definitions, 0 abbreviations, 2 lemmas, 6 theorems)
  • Examples: 0
  • Total complexity: 15109
• Quantifiers
  • Difficulty: hard (2 definitions, 0 abbreviations, 3 lemmas, 4 theorems)
  • Examples: 0
  • Total complexity: 30203