5.1 First-order logic and quantifiers

First-order logic builds on propositional logic, adding quantifiers and predicates to express more complex ideas. It's a powerful tool for formalizing mathematical statements and reasoning about relationships between objects in a given domain.

The syntax of first-order logic includes logical connectives, quantifiers, and predicates. Its semantics deal with interpretations and truth values. Understanding these basics is crucial for translating natural language into logical formulas and reasoning effectively within the system.

First-Order Logic Fundamentals

Syntax and semantics of first-order logic

• Syntax of first-order logic
  • Logical connectives: $\neg, \land, \lor, \rightarrow, \leftrightarrow$ represent negation, conjunction, disjunction, implication, and biconditional
  • Quantifiers: $\forall$ (universal) means "for all", $\exists$ (existential) means "there exists"
  • Variables, constants, functions, and predicates form building blocks of formulas
  • Well-formed formulas (WFFs) constructed using specific rules
    • Atomic formulas consist of predicates applied to terms
    • Complex formulas built from atomic formulas using connectives and quantifiers
• Semantics of first-order logic
  • Interpretation of symbols assigns meaning to logical expressions
    • Domain of discourse defines set of objects under consideration
    • Assignment of truth values to atomic formulas based on interpretation
  • Satisfaction of formulas determined by truth values under given interpretation
  • Models and structures provide concrete realizations of abstract logical theories
• Quantifier semantics
  • Universal quantifier true when formula holds for every element in domain
  • Existential quantifier true when formula holds for at least one element in domain

Translation to first-order logic

• Identifying predicates and their arguments extracts key relationships from statements
• Representing relationships between objects captures complex interactions
• Translating quantifiers
  • "All" or "every" expressed using $\forall$ (All cats are mammals)
  • "Some" or "there exists" conveyed using $\exists$ (Some birds can fly)
• Handling negations and complex statements requires careful analysis of sentence structure
• Common translation patterns
  • Conditional statements often use implication (If it rains, the grass gets wet)
  • Biconditional statements express equivalence (A triangle is equilateral if and only if all its sides are equal)
  • Nested quantifiers handle multiple levels of quantification (Every person has a parent)

Reasoning in First-Order Logic

Rules of inference in first-order logic

• Universal instantiation (UI) applies universal statement to specific instance
• Existential generalization (EG) infers existence from specific instance
• Universal generalization (UG) generalizes from arbitrary instance to universal statement
• Existential instantiation (EI) introduces new constant symbol for existential claim
• Modus ponens and modus tollens with quantifiers extend propositional rules to first-order logic
• Hypothetical syllogism in first-order logic chains implications
• Resolution in predicate logic generalizes propositional resolution
• Substitution of equals replaces terms with equivalent expressions

Validity and satisfiability concepts

• Validity in first-order logic
  • Tautologies and valid formulas true under all interpretations
  • Difference between propositional and first-order validity lies in quantification
• Satisfiability
  • Models and interpretations that satisfy a formula make it true
  • Difference between satisfiable and valid formulas: satisfiable true in some models, valid true in all
• Logical consequence
  • Semantic entailment defines when one formula follows from others
  • Syntactic derivability establishes provability using inference rules
• Soundness and completeness of first-order logic ensure correspondence between syntax and semantics
• Limitations of first-order logic
  • Undecidability of validity means no algorithm can determine validity for all formulas
  • Semi-decidability of logical consequence allows for partial algorithmic solutions