LARA

First-Order Logic

First-order logic is a very powerful notation that extends propositional logic. Here we give only an informal overview of first-order logic, which should be enough for you to understand the meaning of first-order logic formulas based on mathematics and natural language. In future lectures we study first-order logic as a formal system and discuss algorithmic questions in more detail.

On top of propositional operations, first-order logic adds:

  • constructs to represent the structure of propositions:
    • equality ( = )
    • predicate symbols ($P$, $Q$, …)
    • function symbols ($f$, $g$, …)
    • first-order variables ($x$, $y$, …) denoting entities in some domain $D$
  • quantifiers “forall” ($\forall$), “exists” ($\exists$)

Uses of first-order logic

  • precisely describe arbitrary mathematical statements (theorems, conjectures, properties)
  • specify program properties
  • represent the meaning of programs
  • represent knowledge about the world (e.g. knowledge bases, semantic web)

Examples

  • An ancestor of my ancestor is also my ancestor: $\forall x. \forall y.\ ((ancestor(x,I) \land ancestor(y,x)) \rightarrow ancestor(y,I))$
  • Grandparent is the parent of a parent: $\forall x. \forall y.\ (grandparent(x,y) \leftrightarrow (\exists z. parent(x,z) \land parent(z,y)))$
  • Property $P$ holds for infinitely many natural numbers: $\forall n. \exists m.\ m > n \land P(m)$
  • $f$ is continuous in point $x_0$: $\forall \varepsilon > 0. \exists \delta > 0. \forall x.\ |x-x_0| < \delta \rightarrow |f(x)-f(x_0)| < \varepsilon$
  • first $k$ array elements are strictly positive, remaining elements are zero: $\forall i. ((0 \le i \land i < k \rightarrow a(i) > 0) \land ((k \le i \land i < N) \rightarrow a(i)=0)$

First-Order Logic Formulas

We build first-order logic formulas by starting from atomic formulas (defined below) and applying propositional operators and quantifiers:

  • atomic formulas are first-order logic formulas
  • if $P$ and $Q$ are first-order formulas, so are $\lnot P$, $P \land Q$, $P \lor Q$, $P \rightarrow Q$, $P \leftrightarrow Q$
  • if $P$ is a first-order formula, so is $\forall x.P$ and $\exists x. P$

For a given value of variables, each formula evaluates to true or false. The rules for propositional operators are exactly as in propositional logic. Quantifiers can be seen as a way of generalizing conjunction and disjunction. First-order variables range over some domain $D$. In the special case of finite domain $D = \{d_1,\ldots,d_k\}$, we have that

\begin{equation*}\begin{array}{l} (\forall x. P(x)) \ \leftrightarrow\ P(d_1) \land \ldots \land P(d_k) \\ (\exists x. P(x)) \ \leftrightarrow\ P(d_1) \lor \ldots \lor P(d_2) \\ \end{array}\end{equation*}

which corresponds to the intuitive definition of terms “for all” and “there exists”. Note, however, that $D$ can be infinite in general (for example: the set of integers or reals).

Atomic formulas evaluate to true or false. We build atomic formulas by applying predicate symbols and equality to terms:

  • if $t_1$ and $t_2$ are terms, then $t_1 = t_2$ is an atomic formula;
  • if $t_1$, …, $t_n$ are terms and $P$ is a predicate symbol that takes $n$ arguments, then $P(t_1,\ldots,t_n)$ is an atomic formula.

Predicates represent relations, for example, we can represent $\leq$ as a binary relation.

Terms denote elements of the domain $D$. We build them starting from variables and constants and applying function symbols:

  • each first-order variable is a term
  • a constant is a term
  • if $t_1,\ldots,t_n$ are terms and $f$ is a function symbol that takes $n$ arguments, then $f(t_1,\ldots,t_n)$ is also a term.

Example of constants are numerals for natural numbers, such as $0, 1, 2, \ldots$. Examples of function symbols are operations such as $+, -, /$.

From above we see that the set of formulas depends on the set of predicate and function symbols. This set is is called vocabulary or language.

Bounded Quantifiers

In general all quantifiers range over some universal domain $D$. To restrict them to subsets of $D$, we can use bounded quantifiers:

  • $\exists x \in S. P(x)$ means $\exists x. (x \in S \land P(x))$
  • $\forall x \in S. P(x)$ means $\forall x. (x \in S \rightarrow P(x))$ (note implication instead of conjunction)

More generally, if $\rho$ is some binary relation written in infix form, such as $<, \le, >, \ge$ we write

  • $\exists x \mathop{\rho} t. P(x)$ meaning $\exists x. (x \mathop{\rho} t \land P(x))$
  • $\forall x \mathop{\rho} t. P(x)$ means $\forall x. (x \mathop{\rho} t \rightarrow P(x))$ (note implication instead of conjunction)

Evaluating First-Order Logic Formulas

To evaluate first-order logic formulas we need to know:

  • the domain set $D$
  • values of first-order variables in the formula
  • interpretation of predicate symbols and function symbols (e.g. does predicate symbol $R$ denote $\leq$ or $<$ or $>$, does binary function symbol $f$ denote $+$ or $-$)

Examples

Consider formula $F$ given by $\forall x. (P(x) \lor P(f(x))$. The formula has one predicate symbol $P$ that takes one urgument (we call it unary) and one unary function symbol $f$. Assume that the domain $D$ is the set of integers and consider two possible interpretations:

  • $P$ denotes property of being an even integer and $f$ denotes the successor function $f(x)=x+1$. Is formula true under this interpretation?
  • $P$ denotes property of being an even integer and $f$ denotes the squaring function $f(x)=x^2$. Is formula true under this interpretation?

Now consider formula $\forall x. \forall y. ((P(x) \land x=f(y)) \rightarrow P(f(y))$ in each of these two interpretations.

(Finite) Validity and Satisfiability of First-Order Logic Formulas

Formula is valid if and only if it evaluates to true for all domains, values of its variables and interpretations of predicate and function symbols.

Formula is satisfiable if and only if it evaluates to true for some domains, values of its variables, interpretation of predicate and function symbols.

Formula is unsatisfiable if and only if it is false for all domains, values of its variables and interpretations of predicate and function symbols.

Note

  • a formula $F$ is unsatisfiable if and only if it is not satisfiable
  • a formula $F$ is valid if and only if $\lnot F$ is unsatisfiable

Answers to some important algorithmic questions (not immediate):

  • There is no algorithm that given a first-order logic formula outputs “yes” when the formula is valid and “no” otherwise - validity of first-order logic formulas is undecidable
  • There exists an enumeration procedure that systematically lists all valid formulas (and only valid formulas) - validity of first-order logic formulas is enumerable

If instead of considering all domains we only consider finite domains (no natural numbers but only e.g. prefixes of natural numbers of the form $\{1,\ldots, n\}$) then we obtain notions of finite validity, finite satisfiability and finite unsatisfiability.

Note that because finite domains are a special case of possible domains, we have the following:

  • if a formula is finitely satisfiable, then it is satisfiable
  • if a formula is valid, then it is also finitely valid

Answers to some important algorithmic questions about finite satisfiability:

  • There is no algorithm that given a first-order logic formula outputs “yes” when the formula is satisfiable and “no” otherwise - finite satisfiability of first-order logic formulas is undecidable
  • There exists an enumeration procedure that systematically lists all finitely satisfiable formulas (and only finitely satisfiable formulas) - finite satisfiability of first-order logic formulas is enumerable

Some Valid First-Order Logic Formulas

If we take a propositional tautology and replace equal propositional variables with equal atomic formulas, we obtain a valid formula. Such formula is called an instance of a tautology.

But there are many other valid formulas. Such formulas are valid laws of thinking that we often use in mathematics (explicitly, or implicitly without mentioning them).

\begin{equation*}\begin{array}{l} (\forall x. (P(x) \land Q(x)) \leftrightarrow ((\forall x. P(x)) \land (\forall x. Q(x))) \\ (\exists x. (P(x) \land Q(x)) \rightarrow ((\exists x. P(x)) \land (\exists x. Q(x))) \\ (\exists x. (P(x) \lor Q(x)) \leftrightarrow ((\exists x. P(x)) \lor (\exists x. Q(x))) \\ ((\forall x. P(x)) \lor (\forall x. Q(x))) \rightarrow (\forall x. (P(x) \lor Q(x)) \\ (\exists x. \forall y. R(x,y)) \rightarrow (\forall y. \exists x. R(x,y)) \\ (\lnot (\exists x. P(x))) \leftrightarrow (\forall x. (\lnot P(x)) \\ (\lnot (\forall x. P(x))) \leftrightarrow (\exists x. (\lnot P(x)) \\ (\lnot (\exists x \rho t. P(x))) \leftrightarrow (\forall x \rho t. (\lnot P(x)) \\ (\lnot (\forall x \rho t. P(x))) \leftrightarrow (\exists x \rho t. (\lnot P(x)) \\ (\forall x. (x=t \rightarrow F(x))) \leftrightarrow F(t) \\ (\exists x. (x=t \land F(x))) \leftrightarrow F(t) \\ \end{array}\end{equation*}

More information