First-order logic provides a powerful framework for expressing complex statements about objects and their relationships. It builds on propositional logic by introducing quantifiers and predicates, allowing for more nuanced and expressive logical formulations.

The syntax of first-order logic consists of symbols, terms, and formulas. These elements combine to create well-formed formulas that can represent intricate logical statements, laying the groundwork for formal reasoning and proof construction in mathematical and philosophical contexts.

Vocabulary

Symbols and Constants

• Predicate symbols represent relations between objects (Loves, IsGreaterThan)
• Function symbols denote functions that map objects to other objects (MotherOf, Successor)
• Constants refer to specific objects in the domain of discourse (Alice, Bob, 0, 1)
• Variables are used to represent arbitrary objects (x, y, z)

Terms and Atomic Formulas

Building Blocks of First-Order Logic

• Terms are expressions that refer to objects
  • Can be constants (a, b, c), variables (x, y, z), or function applications (f(x), g(a, y))
  • Function applications consist of a function symbol followed by a tuple of terms (MotherOf(Alice), Successor(0))
• Atomic formulas are the simplest type of well-formed formulas in first-order logic
  • Formed by applying a predicate symbol to a tuple of terms (Loves(Alice, Bob), IsGreaterThan(x, y))
  • Represent basic assertions about objects and their relations

Logical Connectives and Quantifiers

Constructing Complex Formulas

• Logical connectives are used to combine simpler formulas into more complex ones
  • Conjunction ($\land$): "and" connects two formulas ($\phi \land \psi$)
  • Disjunction ($\lor$): "or" connects two formulas ($\phi \lor \psi$)
  • Implication ($\rightarrow$): "if...then" connects two formulas ($\phi \rightarrow \psi$)
  • Negation ($\lnot$): "not" negates a formula ($\lnot \phi$)
• Quantifiers express properties about collections of objects
  • Universal quantifier ($\forall$): "for all" specifies that a formula holds for all objects ($\forall x \, \phi(x)$)
  • Existential quantifier ($\exists$): "there exists" specifies that a formula holds for at least one object ($\exists x \, \phi(x)$)

Well-formed Formulas

Syntactically Correct Formulas

• Well-formed formulas (wffs) are syntactically correct expressions in first-order logic
  • Atomic formulas are wffs
  • If $\phi$ and $\psi$ are wffs, then so are ($\phi \land \psi$), ($\phi \lor \psi$), ($\phi \rightarrow \psi$), and ($\lnot \phi$)
  • If $\phi$ is a wff and $x$ is a variable, then $\forall x \, \phi$ and $\exists x \, \phi$ are also wffs
• Free and bound variables
  • A variable $x$ is bound in a formula if it falls within the scope of a quantifier ($\forall x$ or $\exists x$)
  • A variable is free if it is not bound by any quantifier
  • In $\forall x \, \exists y \, (P(x) \land Q(x,y,z))$, $x$ and $y$ are bound, while $z$ is free
• Scope of quantifiers
  • The scope of a quantifier is the portion of the formula it applies to
  • In $\forall x \, (P(x) \land \exists y \, Q(x,y))$, the scope of $\forall x$ is the entire formula, while the scope of $\exists y$ is $Q(x,y)$