Quantifiers are powerful tools in first-order logic, allowing us to express statements about all or some elements in a domain. They come in two flavors: universal (∀) for "all" and existential (∃) for "some."

Negating quantifiers flips their meaning, turning "all" into "some not" and "some" into "none." This property is crucial for understanding logical relationships and constructing valid arguments in first-order logic.

Quantifiers

Universal and Existential Quantifiers

• Universal quantifier $\forall$ expresses that a formula holds for all values of a variable
  • Formally, $\forall x P(x)$ means that $P(x)$ is true for every possible value of $x$ in the domain
  • Can be read as "for all", "for every", or "for each" ($\forall x \in \mathbb{N}, x \geq 0$ reads "for all natural numbers $x$, $x$ is greater than or equal to $0$")
• Existential quantifier $\exists$ expresses that a formula holds for at least one value of a variable
  • Formally, $\exists x P(x)$ means that there exists at least one value of $x$ in the domain for which $P(x)$ is true
  • Can be read as "there exists", "for some", or "there is at least one" ($\exists x \in \mathbb{R}, x^2 = 4$ reads "there exists a real number $x$ such that $x$ squared equals $4$")

Quantifier Negation

• Negation of a universally quantified formula $\forall x P(x)$ is equivalent to an existentially quantified negation of the formula $\exists x \neg P(x)$
  • $\neg(\forall x P(x)) \equiv \exists x \neg P(x)$ (reads "not for all $x$, $P(x)$" is equivalent to "there exists an $x$ such that not $P(x)$")
  • Example: $\neg(\forall x \in \mathbb{N}, x > 0) \equiv \exists x \in \mathbb{N}, x \leq 0$ (reads "not all natural numbers are greater than $0$" is equivalent to "there exists a natural number less than or equal to $0$")
• Negation of an existentially quantified formula $\exists x P(x)$ is equivalent to a universally quantified negation of the formula $\forall x \neg P(x)$
  • $\neg(\exists x P(x)) \equiv \forall x \neg P(x)$ (reads "there does not exist an $x$ such that $P(x)$" is equivalent to "for all $x$, not $P(x)$")
  • Example: $\neg(\exists x \in \mathbb{Z}, x^2 = 2) \equiv \forall x \in \mathbb{Z}, x^2 \neq 2$ (reads "there does not exist an integer $x$ such that $x$ squared equals $2$" is equivalent to "for all integers $x$, $x$ squared does not equal $2$")

Quantifier Transformations

Quantifier Distribution and Elimination

• Quantifier distribution refers to the rules for distributing quantifiers over logical connectives
  • $\forall x (P(x) \land Q(x)) \equiv (\forall x P(x)) \land (\forall x Q(x))$ (universal quantifier distributes over conjunction)
  • $\exists x (P(x) \lor Q(x)) \equiv (\exists x P(x)) \lor (\exists x Q(x))$ (existential quantifier distributes over disjunction)
  • However, $\forall x (P(x) \lor Q(x)) \not\equiv (\forall x P(x)) \lor (\forall x Q(x))$ and $\exists x (P(x) \land Q(x)) \not\equiv (\exists x P(x)) \land (\exists x Q(x))$
• Quantifier elimination is the process of removing quantifiers from a formula while preserving its satisfiability
  • One approach is to replace the quantified variable with a constant that satisfies the formula, if such a constant exists
  • Example: $\exists x (x > 0 \land \forall y (y > x \to y > 1))$ can be simplified to $\exists x (x > 0 \land x < 1)$ by eliminating the universal quantifier

Prenex Normal Form and Skolemization

• Prenex normal form is a formula where all quantifiers appear at the beginning, followed by a quantifier-free matrix
  • Any formula can be converted to prenex normal form by applying quantifier distribution and renaming variables to avoid name clashes
  • Example: $\forall x \exists y (P(x) \lor Q(y))$ is in prenex normal form, while $(\forall x P(x)) \lor (\exists y Q(y))$ is not
• Skolemization is a process of eliminating existential quantifiers from a formula in prenex normal form
  • Each existentially quantified variable is replaced by a Skolem function that depends on the universally quantified variables preceding it
  • The resulting formula is satisfiable if and only if the original formula is satisfiable
  • Example: $\forall x \exists y P(x, y)$ can be Skolemized to $\forall x P(x, f(x))$, where $f$ is a Skolem function