🤔Mathematical Logic Unit 4 – First–Order Logic (Predicate Logic)

Key Concepts and Terminology

• First-order logic (FOL) extends propositional logic by introducing quantifiers, variables, and predicates
• Predicates are symbols that represent relations or properties of objects (e.g., $P(x)$ could represent "$x$ is prime")
• Variables are symbols that stand for objects in the domain of discourse (e.g., $x$, $y$, $z$)
• Constants are symbols that represent specific objects in the domain (e.g., $a$, $b$, $c$)
• Functions are symbols that map objects to other objects (e.g., $f(x)$ could represent "the father of $x$")
• Terms are variables, constants, or functions applied to terms (e.g., $x$, $a$, $f(x)$, $g(a, f(y))$)
• Atomic formulas are predicates applied to terms (e.g., $P(x)$, $Q(a, f(y))$)
• Complex formulas are built from atomic formulas using logical connectives ($\neg$, $\wedge$, $\vee$, $\rightarrow$, $\leftrightarrow$) and quantifiers ($\forall$, $\exists$)

Syntax of First-Order Logic

• The syntax of FOL specifies the rules for constructing well-formed formulas (wffs)
• Variables, constants, and predicates are chosen from disjoint sets of symbols
• Terms are defined recursively:
  • Variables and constants are terms
  • If $f$ is an $n$-ary function and $t_1, \ldots, t_n$ are terms, then $f(t_1, \ldots, t_n)$ is a term
• Atomic formulas are of the form $P(t_1, \ldots, t_n)$, where $P$ is an $n$-ary predicate and $t_1, \ldots, t_n$ are terms
• Complex formulas are built using the following rules:
  • If $\phi$ is a formula, then $\neg \phi$ is a formula
  • If $\phi$ and $\psi$ are formulas, then $(\phi \wedge \psi)$, $(\phi \vee \psi)$, $(\phi \rightarrow \psi)$, and $(\phi \leftrightarrow \psi)$ are formulas
  • If $\phi$ is a formula and $x$ is a variable, then $\forall x \phi$ and $\exists x \phi$ are formulas
• Parentheses are used to disambiguate the structure of formulas

Semantics and Interpretations

• The semantics of FOL assigns meaning to the symbols and formulas
• An interpretation $\mathcal{I}$ consists of a non-empty domain $D$ and a function that maps:
  • Constants to elements of $D$
  • $n$-ary functions to functions from $D^n$ to $D$
  • $n$-ary predicates to subsets of $D^n$
• A variable assignment $s$ is a function that maps variables to elements of $D$
• The value of a term $t$ under an interpretation $\mathcal{I}$ and assignment $s$, denoted $\mathcal{I}_{s}(t)$, is defined recursively:
  • If $t$ is a variable $x$, then $\mathcal{I}_{s}(t) = s(x)$
  • If $t$ is a constant $c$, then $\mathcal{I}_{s}(t) = \mathcal{I}(c)$
  • If $t$ is $f(t_1, \ldots, t_n)$, then $\mathcal{I}_{s}(t) = \mathcal{I}(f)(\mathcal{I}_{s}(t_1), \ldots, \mathcal{I}_{s}(t_n))$
• The truth value of a formula $\phi$ under an interpretation $\mathcal{I}$ and assignment $s$, denoted $\mathcal{I} \models_{s} \phi$, is defined recursively:
  • $\mathcal{I} \models_{s} P(t_1, \ldots, t_n)$ iff $(\mathcal{I}_{s}(t_1), \ldots, \mathcal{I}_{s}(t_n)) \in \mathcal{I}(P)$
  • $\mathcal{I} \models_{s} \neg \phi$ iff $\mathcal{I} \not\models_{s} \phi$
  • $\mathcal{I} \models_{s} (\phi \wedge \psi)$ iff $\mathcal{I} \models_{s} \phi$ and $\mathcal{I} \models_{s} \psi$
  • $\mathcal{I} \models_{s} (\phi \vee \psi)$ iff $\mathcal{I} \models_{s} \phi$ or $\mathcal{I} \models_{s} \psi$
  • $\mathcal{I} \models_{s} (\phi \rightarrow \psi)$ iff $\mathcal{I} \not\models_{s} \phi$ or $\mathcal{I} \models_{s} \psi$
  • $\mathcal{I} \models_{s} (\phi \leftrightarrow \psi)$ iff $\mathcal{I} \models_{s} \phi$ iff $\mathcal{I} \models_{s} \psi$
  • $\mathcal{I} \models_{s} \forall x \phi$ iff for all $d \in D$, $\mathcal{I} \models_{s[x \mapsto d]} \phi$
  • $\mathcal{I} \models_{s} \exists x \phi$ iff there exists $d \in D$ such that $\mathcal{I} \models_{s[x \mapsto d]} \phi$

Quantifiers and Variables

• Quantifiers are logical symbols that express the quantity of objects that satisfy a given formula
• The universal quantifier $\forall$ ("for all") asserts that a formula holds for all objects in the domain
  • Example: $\forall x (P(x) \rightarrow Q(x))$ means "for every $x$, if $P(x)$ holds, then $Q(x)$ holds"
• The existential quantifier $\exists$ ("there exists") asserts that a formula holds for at least one object in the domain
  • Example: $\exists x (P(x) \wedge Q(x))$ means "there exists an $x$ such that both $P(x)$ and $Q(x)$ hold"
• Variables are symbols that stand for arbitrary objects in the domain
• A variable is called free if it is not bound by a quantifier
  • Example: in $\forall x (P(x) \rightarrow Q(y))$, $x$ is bound, but $y$ is free
• A formula with no free variables is called a sentence
• The scope of a quantifier is the formula it quantifies over
  • Example: in $\forall x (P(x) \rightarrow \exists y Q(x, y))$, the scope of $\forall x$ is $(P(x) \rightarrow \exists y Q(x, y))$, and the scope of $\exists y$ is $Q(x, y)$
• Quantifiers can be nested, allowing for complex statements about objects and their relationships

Formal Proofs and Inference Rules

• Formal proofs are sequences of formulas, each of which is either an axiom or derived from previous formulas using inference rules
• Inference rules are syntactic rules that allow new formulas to be derived from existing ones
• Some common inference rules in FOL include:
  • Modus ponens: from $\phi$ and $\phi \rightarrow \psi$, infer $\psi$
  • Universal instantiation: from $\forall x \phi$, infer $\phi[x \mapsto t]$ for any term $t$
  • Existential generalization: from $\phi[x \mapsto t]$, infer $\exists x \phi$
  • Conjunction introduction: from $\phi$ and $\psi$, infer $\phi \wedge \psi$
  • Conjunction elimination: from $\phi \wedge \psi$, infer $\phi$ (or $\psi$)
• A proof system is sound if every formula derivable in the system is logically valid
• A proof system is complete if every logically valid formula is derivable in the system
• Gödel's completeness theorem states that FOL is complete: if a formula is logically valid, then it has a formal proof

Validity and Satisfiability

• A formula $\phi$ is satisfiable if there exists an interpretation $\mathcal{I}$ and an assignment $s$ such that $\mathcal{I} \models_{s} \phi$
  • Example: $\exists x P(x)$ is satisfiable, as there is an interpretation with a non-empty domain and an object that satisfies $P$
• A formula $\phi$ is unsatisfiable if there is no interpretation $\mathcal{I}$ and assignment $s$ such that $\mathcal{I} \models_{s} \phi$
  • Example: $\forall x P(x) \wedge \exists x \neg P(x)$ is unsatisfiable, as no object can both satisfy and not satisfy $P$
• A formula $\phi$ is logically valid (or a tautology) if for every interpretation $\mathcal{I}$ and assignment $s$, $\mathcal{I} \models_{s} \phi$
  • Example: $\forall x (P(x) \vee \neg P(x))$ is logically valid, as every object either satisfies $P$ or does not satisfy $P$
• A formula $\phi$ is logically invalid if there exists an interpretation $\mathcal{I}$ and an assignment $s$ such that $\mathcal{I} \not\models_{s} \phi$
• Logical validity and satisfiability are related: a formula is logically valid iff its negation is unsatisfiable
• Determining the satisfiability or validity of FOL formulas is an undecidable problem in general

Applications and Examples

• FOL is used to formalize and reason about statements in various domains, such as mathematics, computer science, and philosophy
• In mathematics, FOL can be used to define and prove theorems about structures like groups, rings, and fields
  • Example: the associativity of a binary operation $*$ can be expressed as $\forall x \forall y \forall z ((x * y) * z = x * (y * z))$
• In computer science, FOL is used in formal specification and verification of software and hardware systems
  • Example: the Hoare triple $\{P\} C \{Q\}$ can be expressed in FOL as $P \rightarrow wp(C, Q)$, where $wp$ is the weakest precondition predicate transformer
• In database theory, FOL is used to define and query relational databases
  • Example: the query "find all employees who work in the sales department" can be expressed as $\exists x (Employee(x) \wedge Department(x, "sales"))$
• FOL can be used to analyze and validate arguments in natural language
  • Example: the argument "all humans are mortal, Socrates is human, therefore Socrates is mortal" can be formalized as $(\forall x (Human(x) \rightarrow Mortal(x)) \wedge Human(Socrates)) \rightarrow Mortal(Socrates)$
• Many other logics, such as second-order logic, modal logic, and temporal logic, are extensions of FOL with additional expressive power

Common Pitfalls and Tips

• Remember to use parentheses to disambiguate the structure of formulas, especially when using multiple connectives or quantifiers
  • Example: $\forall x P(x) \rightarrow Q(x)$ is different from $\forall x (P(x) \rightarrow Q(x))$
• Be careful with the order of quantifiers, as it can significantly change the meaning of a formula
  • Example: $\forall x \exists y P(x, y)$ is not equivalent to $\exists y \forall x P(x, y)$
• When using multiple quantifiers, ensure that each variable is bound by a quantifier before it is used
  • Example: $\forall x \exists y P(x, y, z)$ is not a well-formed formula if $z$ is not bound by a quantifier
• Keep in mind that the domain of discourse can affect the truth value of a formula
  • Example: $\forall x \exists y (x < y)$ is true in the domain of natural numbers but false in the domain of integers
• Use the negation of quantifiers to express complex statements more concisely
  • Example: $\neg \forall x P(x)$ is equivalent to $\exists x \neg P(x)$, and $\neg \exists x P(x)$ is equivalent to $\forall x \neg P(x)$
• Break down complex formulas into smaller, more manageable parts when analyzing or proving them
  • Example: to prove $\forall x (P(x) \rightarrow (Q(x) \wedge R(x)))$, prove $\forall x (P(x) \rightarrow Q(x))$ and $\forall x (P(x) \rightarrow R(x))$ separately
• Practice translating natural language statements into FOL and vice versa to develop a better understanding of the logic and its applications