3 - First-order logic

Summary

We assume the reader is familiar with first-order logic. Nevertheless, we feel it worthwhile to collect the main definitions and results in the present chapter so that we may refer to them throughout the remainder of the book. Doing so will serve the dual purpose of making the book self-contained and preparing the reader for what lies ahead.

Syntax

Let {x₀, x₁, x₂, …} be a countably infinite set of variables. We will use x, y, z, … as meta-variables ranging over the variables in this set. The symbols U, V, W, … range over finite sets of variables.

Definition 3.1 A vocabulary is a set of relation symbols and function symbols. Each symbol is associated with a natural number, called its arity, that indicates the number of arguments the symbol accepts. Nullary function symbols are called constant symbols, and will often be treated separately. Unary relation symbols are sometimes called predicates.

The function symbols in a vocabulary can be combined with variables to form more complicated expressions called terms.

Definition 3.2 Let L be a vocabulary. The set of L-terms is generated by the finite application of the following rules:

• Every variable is an L-term.

• Every constant symbol in L is an L-term.

• If f is an n-ary function symbol in L and t₁, …, t_n are L-terms, then f(t₁, …, t_n) is an L-term.