First-order logic

First-order logic (FOL) is a type of logical language. It is the most expressive language that has a somewhat “appropriate” automated inference procedure, called resolution. FOL must be defined with the following components:

• A set $V$ of variables. These represent objects in the domain.
• A set $F$ of function symbols. These map objects to other objects (like sit(John, chair)).
  • 0-ary function symbols are called constant symbols.
• A set $P$ of predicate (relation) symbols. These evaluate to true/false and are defined over terms.

From here, we make a few more definitions:

• Terms denote any expression that represents an element in the universe. These are constructed with variables and functions. For example: x, 5, f(g(x, y)).
• Atomic formulas are predicate symbols applied to terms. These are the simplest well-formed formula that can have a truth value. Predicates form atomic symbols. These denote properties and relations that hold about the elements in the universe.
  • The “atomic” comes from a lack of logical symbols (AND, OR) in the formulas.
  • $P(t_1,\cdots ,t_n)$ is true in $\mathcal{M}$ if objects assigned to $t_1,\cdots ,t_n$ are related to each other by $P^{\mathcal{M}}$.
• Formulas are expressions that evaluate to true or false. These themselves can be atomic formulas or built from atomic formulas using logical operators.
  • We can create complex assertions by composing atomic formulas.
  • Their truth is dependent on the truth of the atomic formulas in them.

A set $\mathcal{L}$ of function and predicate symbols is called a first-order vocabulary. Note that variables are not part of the vocabulary. We can construct this set recursively:

• Base: Every variable is a term.
• Recursion: If $f$ is an $n$-ary function symbol in $\mathcal{L}$ and $t_1,t_2,\cdots ,t_n$ are $\mathcal{L}$-terms, then $f(t_1,t_2,\cdots ,t_n)$ is a $\mathcal{L}$-term.
  • So long as we have a function symbol with $n>0$ variables, then the number of terms we can generate is infinite.

The set of first-order $\mathcal{L}$-formulas (syntax) is defined recursively. We have two more operators than in propositional logic.

• Atomic formulas: $P(t_1,t_2,\cdots ,t_n)$, where $P$ is an $n$-ary predicate symbol in $\mathcal{L}$ and $t_1,t_2,\cdots ,t_n$ are $\mathcal{L}$-terms.
• Negation: $\neg f$, where $f$ is a $\mathcal{L}$-formula.
• Conjunction: $f_1\wedge f_2\wedge \cdots \wedge f_n$, where $f_1,f_2,\cdots ,f_n$ are $\mathcal{L}$-formulas.
• Disjunction: $f_1\vee f_2\vee \cdots \vee f_n$, where $f_1,f_2,\cdots ,f_n$ are $\mathcal{L}$-formulas.
• Implication: $f_1\to f_2$, where $f_1,f_2$ are $\mathcal{L}$-formulas.
• Existential: $\exists xf$, i.e., there exists some $x$ such that $f$ is true, where $x$ is a variable and $f$ is a $\mathcal{L}$-formula.
• Universal: $\forall xf$, where $x$ is a variable and $f$ is a $\mathcal{L}$-formula.

Conversion from natural language

Some basic representations:

• Individuals/constants/0-ary functions: rain, snow, names (Tony, Mike, Nick).
• Types: unary predicates
  • $S(x)$ might indicate that $x$ is a skier.
• Relationships: binary predicates
  • $L(x,y)$ might indicate that $x$ likes $y$.

Some tips:

• For separate predicates, we can translate them separately, then combine them with a conjunction/disjunction/implication.
• If the statement says “all” or “whatever”, that’s a good sign to use the universal operator.
• “Is there an x that predicate?”, we can use $\exists$.

Structures

Each FOL interpretation should:

• Specify the objects in the world.
• Settle which objects satisfy predicate $P$.
• Assigns to a function $f$ a mapping from objects to objects (assuming functions are always well-defined and single-valued).

Let $\mathcal{L}$ be a first-order vocabulary. An $\mathcal{L}$-structure $\mathcal{M}$ consists of the following:

• A non-empty set $M$ called the universe (or domain) of discourse.
• For each $n$-ary predicate symbol $P\in \mathcal{L}$, an associated relation $P^{\mathcal{M}}\subseteq M^n$. $P^{\mathcal{M}}$ is called the extension or interpretation of the predicate symbol $P$ in $\mathcal{M}$.
• For each $n$-ary function symbol $f\in \mathcal{L}$, an associated function $f^{\mathcal{M}}:M^n\to M$. $f^{\mathcal{M}}$ is called the extension or interpretation of the function symbol $f$ in $\mathcal{M}$.
  • If $n=0$, then $f$ is a constant symbol and $f^{\mathcal{M}}$ is simply an element of $M$.

$\mathcal{M}$ is essentially a world configuration.

Sometimes, our formula may only be satisfied for certain variables in the domain. In this case, we must assign the objects. Let $\mathcal{M}$ be a structure and $X$ be a set of variables. An object assignment $\sigma$ for $\mathcal{M}$ is a mapping from variables in $X$ to the universe of $\mathcal{M}$.

However, sometimes we must extend this to function symbols (imagine a nested function $f(g(x))$. The extension $\bar{\sigma }$ of $\sigma$ is defined recursively:

• For every variable $x$, $\bar{\sigma }(x)=\sigma (x)$.
• For every function symbol $f\in \mathcal{L},\bar{\sigma }(f(t_1,\cdots ,t_n))=f^{\mathcal{M}}(\bar{\sigma }(t_1),\cdots ,\bar{\sigma }(t_n))$.

For an $\mathcal{L}$-formula $C$, $\mathcal{M}\models C[\sigma ]$ (i.e., $\mathcal{M}$ satisfies $C$ under $\sigma$, or $\mathcal{M}$ is a model of $C$ under $\sigma$) is defined recursively on the structure of $C$ as follows, assuming $A,B$ are $\mathcal{L}$-formulas:

• $\mathcal{M}\models P(t_1,\cdots ,t_n)[\sigma ]⟺⟨\bar{\sigma }(t_1),\cdots ,\bar{\sigma }(t_n)⟩\in P^{\mathcal{M}}$
  • A predicate symbol $P$ applied to terms $t_1,\cdots ,t_n$ is satisfied if the tuple of values assigned to those terms belong to the interpretation of $P$ in the model $\mathcal{M}$.
• $\mathcal{M}\models (s=t)[\sigma ]⟺\bar{\sigma }(s)=\bar{\sigma }(t)$
  • An equality is satisfied if both terms evaluate to the same value in the assignment.
• $\mathcal{M}\models \neg A[\sigma ]⟺\mathcal{M}⊭A[\sigma ]$
  • Negation is satisfied if the formula being negated is not satisfied.
• $\mathcal{M}\models (A\vee B)[\sigma ]⟺\mathcal{M}\models A[\sigma ]\text{or}\mathcal{M}\models B[\sigma ]$
  • A disjunction (OR) is satisfied if at least one of the disjuncts is satisfied.
• $\mathcal{M}\models (A\wedge B)[\sigma ]⟺\mathcal{M}\models A[\sigma ]\text{and}\mathcal{M}\models B[\sigma ]$
  • A conjunction (AND) is satisfied if both conjuncts are satisfied.
• $\mathcal{M}\models (\forall xA)[\sigma ]⟺\mathcal{M}\models A[\sigma (m/x)]\forall m\in M$
  • A universal quantification is satisfied if the formula is satisfied for every possible value in the domain.
• $\mathcal{M}\models (\exists xA)[\sigma ]⟺\mathcal{M}\models A[\sigma (m/x)]\text{for some}m\in M$
  • An existential quantification is satisfied if the formula is satisfied for at least one value in the domain.

A structure $\mathcal{M}$ satisfies $\Phi$ (a set of sentences), denoted by $\mathcal{M}\models \Phi$ if for every sentence $A\in \Phi$, $\mathcal{M}\models A$. If $\mathcal{M}\models \Phi$, we say $\mathcal{M}$ is a model of $\Phi$. We say that $\Phi$ is satisfiable if there is a structure $\mathcal{M}$ such that $\mathcal{M}\models \Phi$.

For a set of sentences $\Phi$, a sentence $A$ is a logical consequence of $\Phi$ (denoted by $\Phi \models A$) iff for every structure $\mathcal{M}$, if $\mathcal{M}\models \Phi$, then $\mathcal{M}\models A$. Alternatively, then there is no $\mathcal{M}$ such that $\mathcal{M}\models \Phi \cup \{\neg A\}$, i.e., $\Phi \cup \{\neg A\}$ is unsatisfiable.

An occurrence of $x$ in $A$ is bounded (is “quantified”) iff it is in a sub-formula of $A$ of the form $\forall xB$ or $\exists xB$. Basically, a variable $x$ is bound if it appears within the scope of a quantifier ($\forall$ or $\exists$) that uses the same variable. The quantifier “binds” the variable, similar to how a parameter in a function definition binds the parameter name to values passed to the function. Otherwise the occurrence is free. For example, the $x$ in $P(x)$ is free, but the $x$ in the other $P(x)$ and $Q(x)$ are bounded by the existential quantifier $\exists x$:

$$P(x)\wedge \exists x[P(x)\vee Q(x)]$$

A formula $A$ is closed if it contains no free occurrence of a variable. A closed formula is called a sentence. If $\sigma$ and ${\sigma }^{\prime }$ agree on the free variables of $A$, then $\mathcal{M}\models A[\sigma ]$ iff $\mathcal{M}\models A[{\sigma }^{\prime }]$. If $A$ is a sentence (no free variables), then $\sigma$ is irrelevant and we omit mention of $\sigma$ and simply write $\mathcal{M}\models A$.