# A crash course in first-order logic

2015.07.13

This is a short but reasonably complete description of first-order logic, a rich system to reason about objects and their relationships. I care mostly about first-order logic for its role in statistical relational learning (a branch of machine learning), which I'll cover in another post. If you want a more detailed explanation, see Russell and Norvig's excellent A.I. book.

## Terms

Terms represent objects and relationships between objects, they are the reason why first-order logic is so flexible. There are three types of terms:

1. Constants represent objects, e.g.: Tokyo, the number 47, Cylon, Lion.
2. Variables range over objects, e.g. the variable c could represent a city, x an integer, s a species. By convention, variables will start with a lowercase character (it's not a universal convention, in fact it's common to have the opposite).
3. Functions map lists of terms to a term, e.g. CapitalOf could take a country and return a city, while Multiply takes two numbers and returns a number.

Example:

$Add(x, 5).$

Add is a function taking two numbers and returning a number, x is a variable, and 5 is a constant. Since a function is a term, it can be used within functions:

$Add(Multiply(x, y), 5).$

## Predicates

First-order logic formulas ultimately resolve to a truth value: True or False, yet the terms we've seen can represent cities, numbers, pretty much anything. To get a truth value, we need predicates. A predicate is like a function but it maps terms to a truth value instead of mapping them to a term. For example, if we want to say that adding 0 to x yields x, we can write:

$Equals(Add(x, 0), x).$

It's common to use the equal sign for the "equals" (or identity) predicate:

$Add(x, 0) = x.$

Equals is a predicate. In this case it takes two numbers and returns true or false. We could have a predicate taking three cities and return true if they are on the same continent:

$SameContinent(Toronto, c, CapitalOf(LargestCountryOf(Europe))),$

where SameContinent is a predicate, Toronto and Europe are constants, c a variable ranging over cities, and both CapitalOf and LargestCountryOf are functions taking a single argument.

## Atomic formulas

An atomic formula is something that, alone, is a valid first-order logic formula. A predicate is an atomic formula since it returns a truth value, but we also have two special symbols: True and False.

True is also called top, and can be represented with the symbol $$\top$$ or just T.

False is also called bottom, and can be represented with the symbol $$\bot$$ or just F.

## Connectives

You can connect formulas with connectives to form complex formulas. The standard connectives are:

1. The binary connective and: $$x \land y$$, which is true only if both $$x$$ and $$y$$ are true. Like all other connectives shown here, if $$x$$ and $$y$$ are valid formulas, then $$x \land y$$ is also a valid formula.
2. The binary connective or: $$x \lor y$$, which is true only if $$x$$ is true, if $$y$$ is true, or if both are true.
3. The binary connective implies: $$x \Rightarrow y$$, returns true in all cases, except if $$x$$ is true and $$y$$ is false.
4. The binary connective iff: $$x \iff y$$, returns true if $$x$$ and $$y$$ have the same value, that is if they are both true, or both false.
5. The binary connective xor (exclusive or): $$x \oplus y$$, returns true if $$x$$ and $$y$$ have different values.
6. The unary connective not: $$\lnot x$$, which is true only if $$x$$ is false.

Be careful with implication, there is nothing wrong with it, except that it doesn't fit how we use the term implies. For example: $$Equals(AgeOf(Earth), 42) \Rightarrow StillAlive(Elvis)$$ is true. If you're confused, read again the description of implies. Here's the truth table for the binary connectives:

Connective Informal name Symbol T x TT x FF x TF x F
Conjunction and $$\land$$ TFFF
Disjunction or $$\lor$$ TTTF
Implication implies $$\Rightarrow$$ TFTT
Equivalence iff $$\leftrightarrow$$ TFFT
Exclusive disjunction xor $$\veebar$$ FTTF

## Quantifiers

There are two quantifiers in first-order logic: the universal quantifier "for all" denoted $$\forall$$, and the existential quantifier "exists" denoted $$\exists$$. They, well, quantify variables, e.g.:

$\forall x: Multiply(x, 0) = 0$

reads "for all x, multiplying x by 0 yields 0". Another example:

$\forall x: Real(x) \Rightarrow (\exists y: y > x)$

which means, "for all real numbers x, there is a number y that is greater than x". Note that both $$Real$$ and the > sign are predicates.

A last example: we can express "there is a color c brighter than x, unless x is white" with:

$\forall x: IsWhite(x) \lor (\exists c: BrighterThan(c, x)).$
let world = "世界" in print \$ "Hello " ++ world ++ "!"