A crash course in first-order logic

Tweet

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

Qualifiers

There are two qualifiers in first-order logic: the universal qualifier "for all" denoted \(\forall\), and the existential qualifier "exists" denoted \(\exists\). They, well, qualify 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 ++ "!"