Logic for Computer Science/First-Order Logic

First-Order Logic

In propositional logic, we considered formulas made about atomic objects, which could only be either true or false. First-order logic, the topic of this chapter, builds upon propositional logic and allows you to look inside the objects discussed in formulas. We can provide this more refined level of granularity by discussing objects as elements of sets that can be larger than just the set $\{0,1\}$, and also include arbitrarily complex relationships with each other.

We begin first by defining the syntax of first-order (FO) logic, and then give these structures meaning.

Syntax

The domain of discourse for first order logic is first-order structures or models. A first-order structure contains

1. Relations,
2. Functions, and
3. Constants (functions of arity 0).

The vocabulary of first-order logic is

1. a set of relation symbols with associated arities, and
2. a set of function symbols with associated arities.

Here are some example first-order logic vocabularies:

1. A graph
   • Relation Set = { $V$ : unary, $E$ : binary }
   • Function Set = { $𝑛𝑒𝑥𝑡$ : unary }
2. Arithmetic
   • Relation Set = { $+$ : ternary, $\times$ : ternary, $\uparrow$ : ternary, $=$ : binary, $<$ : binary}
   • Function Set = { $𝑛𝑒𝑥𝑡$ : unary, $0$ : const }

Here, a graph is a set of vertices $V$ and a set of edges $E$. For the arithmetic set note that the use of $+$ and $\times$ is purely syntactic and we could have used the symbols "plus" and "times" instead. We haven't provided the symbols with any meaning yet.

A term denotes an element in the first-order structure. A term is used to refer to the elements in our domain of discourse. Here are the rules that describe what a term is:

• every variable is a term, where a variable is simply another set of symbols
• every constant is a term
• If $t_1,t_2,\dots ,t_k$ are terms, and $f$ is a $k$-ary function then $f(t_1,t_2,\dots ,t_k)$ is a term.

For example, if $f$ is a binary function and $g$ is a ternary function then the following are all terms: $x,a,f(x,y),g(x,f(x,y),a)$.

An atomic formula is

$R(t_1,t_2,\dots ,t_k)$,

where $R$ is a $k$-ary relation and $t_1,t_2,\dots ,t_k$ are terms. When viewing $R$ as a set, then this is just another way of saying that the tuple

$(t_1,t_2,\dots ,t_k)\in R$.

A special relation $=$ means "equal" and cannot be interpreted otherwise. For example, $t_1=t_2$ stands for

$=(t_1,t_2)$.

A first-order formula is an expression built using a given first-order vocabulary and variables and the symbols $(,),\mathrm{\neg },\vee ,\wedge ,\to ,\mathrm{\exists },\mathrm{\forall }$. The set of first-order formulas is the minimum set satisfying the following:

• atomic formulas are first order formulas
• If $\varphi$ and $\psi$ are formulas and $x$ is a variable, then the following are also formulas:

1. $(\varphi \vee \psi )$
2. $(\varphi \wedge \psi )$
3. $(\mathrm{\neg }\varphi )$
4. $(\varphi \to \psi )$
5. $(\mathrm{\exists }x\varphi )$
6. $(\mathrm{\forall }x\varphi )$

Semantics

A first-order structure over a given vocabulary consists of

1. A domain, which is a set of elements (also known as a universe)
2. A mapping associating to every $k$-ary relation symbol in the vocabulary a $k$-ary relation over the domain, and to every $k$-ary function symbol a $k$-ary function over the domain.

These components give meaning to the symbols.

Example:

Relation Set = { $+$ : ternary, $\times$ : ternary, $\uparrow$ : ternary, $=$ : binary, $<$ : binary }

Function Set = { $next$ : unary, $0$ : const }

A first-order structure over this vocabulary is:

1. Domain: the set of integers
2. Mapping : $+\to$ addition, $\times \to$ multiplication, $\uparrow \to$ exponentiation, $<\to$ ordering, $𝑛𝑒𝑥𝑡\to i+1$

In this structure, the formula

$\mathrm{\exists }x\mathrm{\forall }y\mathrm{\forall }z[\times (y,z,x)\to ((y=1)\vee (z=1))]$

expresses the statement "there exists a prime number" (the number 1 also satisfies this statement).

Note here that $\times (y,z,x)$ is equivalent to $(x=y\times z)$.

Scope of Quantifiers

In the formula $(\mathrm{\forall }x\varphi )$ or $(\mathrm{\exists }x\varphi )$, $\varphi$ is referred to as the scope of quantification of the variable $x$. An occurrence of a variable in a formula is bound if it is in the scope of quantification of that variable, otherwise the occurrence is said to be free. You can consider a quantifier use as a variable declaration.

A sentence is a formula with no free variables (i.e., all variables are bound). A sentence is either true or false.

A formula with free variable(s) can be considered as describing the properties of the free variable(s). For example, $\varphi (x)$ denotes a formula with $x$ occurring free and describes the properties of $x$.

If a sentence $\varphi$ evaluates to true over a structure $I$, we say $I$ satisfies $\varphi$ and denote this by $I\models \varphi$.

• $I\models R(t_1,t_2,\dots ,t_k)$ iff $(t_1,t_2,\dots ,t_k)\in I(R)$, where $I(R)$ is the interpretation of $R$ by $I$.
• $I\models \varphi \wedge \psi$ iff $I\models \varphi$ and $I\models \psi$. (Similar for $\vee$.)
• $I\models \mathrm{\neg }\phi$ iff $I\models ̸\phi$.
• $I\models \mathrm{\exists }x\varphi (x)$ if $I\models \varphi (x\leftarrow c)$ for some $c$ in the domain.
• $I\models \mathrm{\forall }x\varphi (x)$ if $I\models \varphi (x\leftarrow c)$ for every $c$ in the domain.

Note: $\varphi (x\leftarrow c)$ denotes the result of substituting $c$ for every free occurrence of $x$ in $\varphi$. Substitution is covered further later in this chapter.

Axiomatic approach

The axioms are a set of sentences meant to distinguish "desired" models from others. But typically, also have "undesired" models, which are called non-standard models.

Examples: Consider the vocabulary $(𝑛𝑒𝑥𝑡,+,\times ,\uparrow ,0,=,<)$, where the symbols have the usual meaning (defined by FO sentences over this vocabulary). The standard interpretation for this set of axioms (see the end of this chapter) is the integers, but these are also satisfied by the set of integers modulo $p$. This possibility is ruled out by adding the following sentence to the axioms: $\mathrm{\forall }x(x<𝑛𝑒𝑥𝑡(x))$

Question: Can all non-standard models be axiomatized away? The answer is no. Consider the model shown in [TODO: import figure] for the vocabulary containing only $0,<,\sigma$ (all elements in the upper line are larger than those on the lower line).

There is no set of first-order sentences that can distinguish this model from the natural numbers. Intuitively, the reason is that we cannot "backtrack" arbitrarily (towards $0$) in a first-order sentence. A similar non-standard model can be obtained for the full vocabulary above.

Evaluating FO Sentences

Given a first-order structure $I$ and a FO sentence $\varphi$, can we tell if $I\models \varphi$?

This problem is decidable for finite structures. For example, suppose $E$ is a binary relation representing the edges of a graph, and the given sentence is

$\mathrm{\exists }{x}_1\mathrm{\exists }{x}_2\mathrm{\exists }{x}_3(E(x_1,x_2)\wedge E(x_2,x_3)\wedge E(x_3,x_1)\wedge x_1\ne x_2\wedge x_2\ne x_3\wedge x_3\ne x_1)$.

We can evaluate the truth of this sentence by trying all possible values for $x_1,x_2$ and $x_3$. (Naive evaluation: "nested loop".) This is polynomial time (in domain size) but exponential in the size of the formula.

On infinite domains, we may or may not be able to evaluate the truth of a sentence. With the vocabulary $(N,0,\sigma ,<,+)$, where $N$ is the set of natural numbers, it is decidable if a sentence is true. (This is known as Presburger arithmetic.) However if we include multiplication, the truth of a sentence becomes undecidable.

A Deductive System for FO

A set $\mathrm{\Delta }$ of FO sentences is

• Satisfiable if there is some structure $I$ such that $I\models \mathrm{\Delta }$
• Unsatisfiable if it is not satisfiable
• Valid if $I\models \mathrm{\Delta }$ for all structure $I$

Given a set of FO sentences $\mathrm{\Sigma }$ and a sentence $\varphi$

• $\mathrm{\Sigma }$ entails $\varphi$ (denoted $\mathrm{\Sigma }\models \varphi$), if every structure that satisfies $\mathrm{\Sigma }$ also satisfies $\varphi$.
• $\mathrm{\Sigma }\models \varphi$ iff $\mathrm{\Sigma }\cup \{\mathrm{\neg }\varphi \}$ is unsatisfiable.
• If $\mathrm{\Sigma }$ is finite then, $\mathrm{\Sigma }\models \varphi$ iff $\mathrm{\neg }\mathrm{\Sigma }\vee \varphi$ is valid.
• If a formula $\varphi$ has free variables $\overrightarrow{X}=(x_1,\dots ,x_k)$, $\varphi$ is valid iff $\mathrm{\forall }\overrightarrow{X}\varphi$ is valid.

Axioms for Validity

The axioms for validity are from three categories:

1. Axioms for boolean validity. These are inherited from propositional logic.
2. Axioms for equality.
3. Axioms for quantification.

Boolean Validity

Given a FO formula $\phi$, a boolean form of $\phi$ a propositional formula $\psi$ such that $\phi$ is obtained from $\psi$ by replacing each propositional variable in $\psi$ by a subformula of $\phi$.

The set of Boolean forms of $\phi$ is denoted $BF(\phi )$.

Examples:

• For the FO formula $\mathrm{\forall }xP(x)\vee \mathrm{\neg }\mathrm{\forall }xP(x)$, the boolean form is $p\vee \mathrm{\neg }p$.
• If $\phi \equiv \mathrm{\forall }xG(x,y)\wedge \mathrm{\exists }xG(x,y)\wedge (G(z,x)\vee \mathrm{\forall }xG(x,y))$, then $BF(\phi )\equiv x_1\wedge x_3\wedge (x_2\vee x_1)$ where $x_1=\mathrm{\forall }xG(x,y),x_2=G(z,x),x_3=\mathrm{\exists }xG(x,y)$.

Claim: If $\psi \in BF(\phi )$ and $\psi$ is valid, then $\phi$ is valid.

Equality Axioms

Let $t,t_1,\dots ,t_k,t{\text{'}}_1,\dots ,t{\text{'}}_k$ be terms. The following are valid formulas.

• $t=t$
• $(t_1=t{\text{'}}_1\wedge \cdots \wedge t_k=t{\text{'}}_k)\to (f(t_1,\dots ,t_k)=f(t{\text{'}}_1,\dots ,t{\text{'}}_k))$, where $f$ is a $k$-ary function.
• $(t_1=t{\text{'}}_1\wedge \cdots \wedge t_k=t{\text{'}}_k)\to (R(t_1,\dots ,t_k)\to R(t{\text{'}}_1,\dots ,t{\text{'}}_k))$, where $R$ is a $k$-ary relation.

Substitutions

Given a formula $\phi$ in which variable $x$ occurs free (denoted by $\phi (x)$) and a term $t$, we define the substitution of $t$ for $x$ in $\phi$, denoted $\phi (x\leftarrow t)$, as the formula that results from replacing every free occurrence of $x$ in $\phi$ by $t$, subject to the constraint that $t$ contains no variable $y$ quantified in $\phi$ such that $x$ occurs free within the scope of quantification of $y$. If $x$ does not occur free $\phi$, then $\phi (x\leftarrow t)$ is defined as $\phi$.

Example: Let $\phi$ be

$((x=1)\to \mathrm{\exists }x(x=y))$,

then

• $\phi (x\leftarrow (y+1))$ is a valid substitution
• $\phi (y\leftarrow (x+1))$ is not a valid substitution.

Quantification Axioms

1. $\mathrm{\forall }x\phi \to \phi (x\leftarrow t)$, where $t$ is a term and $\phi (x\leftarrow t)$ is a valid substitution
2. $(\mathrm{\forall }x(\phi \to \psi ))\to ((\mathrm{\forall }x\phi )\to (\mathrm{\forall }x\psi ))$
3. $\phi \to \mathrm{\forall }x\phi$
4. $\mathrm{\exists }x\phi \leftrightarrow \mathrm{\neg }\mathrm{\forall }x\mathrm{\neg }\phi$

In summary, the axioms for validity are $𝐀𝐱$:

1. Axioms for boolean validity. These are inherited from propositional logic.
2. Axioms for equality.
3. Axioms for quantification.

Definition: A proof is a sequence ${\varphi }_1,{\varphi }_2,\dots ,{\varphi }_k$ of FO sentences such that for each $i\in \{1,\dots ,k\}$ either ${\varphi }_i\in 𝐀𝐱$ or $\mathrm{\exists }j,k<i$ such that ${\varphi }_j\equiv \psi$ and ${\varphi }_k\equiv (\psi \to {\varphi }_i)$.

Notation: If there is a proof of $\varphi$ using $𝐀𝐱$, we denote this fact by ${⊢}_{𝐀𝐱}\varphi$.

Fact (Soundness): If ${⊢}_{𝐀𝐱}\varphi$, then $\varphi$ is valid.

Remark: The set of formulas which can be proven valid is recursively enumerable.

Example: Proof of the formula $\mathrm{\forall }x(\varphi \wedge \psi )\to (\mathrm{\forall }x\varphi \wedge \mathrm{\forall }x\psi )$

$\mathrm{\forall }x(\varphi \wedge \psi )$

$\mathrm{\forall }x(\varphi \wedge \psi )\to (\varphi \wedge \psi )(x\leftarrow x)$

$\varphi \wedge \psi$

$\varphi$

$\mathrm{\forall }x(\varphi \wedge \psi )\to \varphi$

$\mathrm{\forall }x(\mathrm{\forall }x(\varphi \wedge \psi )\to \varphi )$

$\mathrm{\forall }x\mathrm{\forall }x(\varphi \wedge \psi )\to \mathrm{\forall }x\varphi$

$\mathrm{\forall }x(\varphi \wedge \psi )\to \mathrm{\forall }x\varphi$

$\mathrm{\forall }x\varphi$

The proof of $\mathrm{\forall }x\psi$ is symmetrical.

$\mathrm{\forall }x\varphi \wedge \mathrm{\forall }x\psi$

$\mathrm{\forall }x(\varphi \wedge \psi )\to (\mathrm{\forall }x\varphi \wedge \mathrm{\forall }x\psi )$

Useful Equivalences

• $\mathrm{\forall }x(\varphi \wedge \psi )\leftrightarrow (\mathrm{\forall }x\varphi )\wedge (\mathrm{\forall }x\psi )$
• $\mathrm{\forall }x(\varphi \vee \psi )\leftrightarrow ̸(\mathrm{\forall }x\varphi )\vee (\mathrm{\forall }x\psi )$ e.g. $\varphi (x)\approx$ "x is even" and $\psi (x)\approx$ "x is odd"
• $\mathrm{\forall }x(\varphi (x)\vee \mathrm{\neg }\varphi (x))\leftrightarrow ̸(\mathrm{\forall }x\varphi (x)\vee \mathrm{\forall }x\mathrm{\neg }\varphi (x))$
• $\mathrm{\exists }x(\varphi \vee \psi )\leftrightarrow (\mathrm{\exists }x\varphi )\vee (\mathrm{\exists }x\psi )$
• $\mathrm{\neg }\mathrm{\exists }x\varphi \leftrightarrow \mathrm{\forall }x\mathrm{\neg }\varphi$
• $\mathrm{\neg }\mathrm{\forall }x\varphi \leftrightarrow \mathrm{\exists }x\mathrm{\neg }\varphi$

Prenex Normal Form

Claim: Every FO sentence is equivalent to a FO sentence of the form $Q_1{x}_1\cdots Q_k{x}_k\varphi$, where $Q_i\in \{\mathrm{\exists },\mathrm{\forall }\}$ and $\varphi$ is quantifier free.

This is proved using the distributive properties of quantifiers. It may be necessary to rename variables, to avoid ambiguities. Although you can always move all quantifiers to the left, the resulting formula can actually be exponentially larger than the original one.

Example:

$\varphi \equiv \mathrm{\forall }x(G(x,x)\wedge (\mathrm{\forall }yG(x,y)\vee \mathrm{\exists }y\mathrm{\neg }G(y,y)))\wedge G(x,0)$

$\equiv (\mathrm{\forall }x(G(x,x)\wedge (\mathrm{\forall }yG(x,y)\vee \mathrm{\exists }y\mathrm{\neg }G(y,y))))\wedge G(w,0)$

$\equiv \mathrm{\forall }x(G(x,x)\wedge (\mathrm{\forall }yG(x,y)\vee \mathrm{\exists }y\mathrm{\neg }G(y,y))\wedge G(w,0))$

$\equiv \mathrm{\forall }x(G(x,x)\wedge (\mathrm{\forall }yG(x,y)\vee \mathrm{\exists }z\mathrm{\neg }G(z,z))\wedge G(w,0))$

$\equiv \mathrm{\forall }x(G(x,x)\wedge \mathrm{\forall }y(G(x,y)\vee \mathrm{\exists }z\mathrm{\neg }G(z,z))\wedge G(w,0))$

$\equiv \mathrm{\forall }x\mathrm{\forall }y(G(x,x)\wedge (G(x,y)\vee \mathrm{\exists }z\mathrm{\neg }G(z,z))\wedge G(w,0))$

$\equiv \mathrm{\forall }x\mathrm{\forall }y(G(x,x)\wedge \mathrm{\exists }z(G(x,y)\vee \mathrm{\neg }G(z,z))\wedge G(w,0))$

$\equiv \mathrm{\forall }x\mathrm{\forall }y\mathrm{\exists }z(G(x,x)\wedge (G(x,y)\vee \mathrm{\neg }G(z,z))\wedge G(w,0))$

Recall the Axiomatic Method

1. Describe the desired model as closely as possible using a (possibly infinite but recursive) set $\mathrm{\Delta }$ of axioms (FO sentences).

1. Prove things using deduction.

Notation: We say $\varphi$ is a valid consequence of $\mathrm{\Delta }$ (denoted $\mathrm{\Delta }\models \varphi$), if every model satisfying $\mathrm{\Delta }$ also satisfies $\varphi$.

Fact: $\mathrm{\Sigma }\models \varphi$ iff $\mathrm{\Sigma }\cup \{\mathrm{\neg }\varphi \}$ is unsatisfiable.

Aside: Nonlogical axioms for number theory

The following fourteen first-order axioms describe the properties of arithmetic and numbers, i.e. addition ($+$), multiplication ($\times$), exponentiation ($\uparrow$, equality ($=$), ordering ($<$), successor function ($\sigma$) and remainder (mod). This example shows the expressive power of first-order statements, which were originally hoped to provide a basis for the "one true mathematics."

Question: Why are they called "nonlogical" axioms?

NT1: $\mathrm{\forall }x(\sigma (x)\ne 0)$

NT2: $\mathrm{\forall }x\mathrm{\forall }y(\sigma (x)=\sigma (y)\to x=y)$

NT3: $\mathrm{\forall }x(x=0\vee \mathrm{\exists }y\sigma (y)=x)$

NT4: $\mathrm{\forall }x(x+0=x)$

NT5: $\mathrm{\forall }x\mathrm{\forall }y(x+\sigma (y)=\sigma (x+y))$

NT6: $\mathrm{\forall }x(x\times 0=0)$

NT7: $\mathrm{\forall }x\mathrm{\forall }y(x\times \sigma (y)=(x\times y)+x)$

NT8: $\mathrm{\forall }x(x\uparrow 0=\sigma (0))$

NT9: $\mathrm{\forall }x\mathrm{\forall }y(x\uparrow \sigma (y)=(x\uparrow y)\times x)$

NT10: $\mathrm{\forall }x(x<\sigma (x))$

NT11: $\mathrm{\forall }x\mathrm{\forall }y(x<y\to (\sigma (x)\le y))$

NT12: $\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\neg }(x<y)\leftrightarrow y\le x)$

NT13: $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z(((x<y)\wedge (y<z))\to x<z)$

NT14: $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z\mathrm{\forall }{z}^{\prime }(mod(x,y,z)\wedge mod(x,y,z^{\prime })\to z=z^{\prime })$