- variables are terms, and
- if t
_{i}are terms for i=1,...,n and f is an n-ary function symbol, then f(t_{1},...,t_{n}) is a term.

- if t
_{i}are terms for i=1,...,n and p is an n-ary predicate symbol, then p(t_{1},...,t_{n}) is a formula. - if P and Q are formulas, then P is a formula, P Q is a formula, P Q is a formula, P Q is a formula, and P <=> Q is a formula.
- if P is a formula and x a variable, then x: P and x: P are formulas.

**Theorem:** It is undecidable whether a first order logic formula
is provable (or true under all possible interpretations).

**Proof:** Suppose there is an algorithm B that, given a first
order logic and a formula in that logic, decides whether that formula
is valid (holds under all possible interpretations). I will use that
to give a decision algorithm for the language {(M,w) | M is the
description of a Turing machine that accepts the string w}. As the
latter problem is undecidable this will show that B cannot exists.

Given M and w, create a first order logic by declaring a constant
, a unary function symbol *a* for every letter *a* in
the alphabet, and a binary predicate f_{q} for every state q
of M.

Consider the following interpretation of this logic:
Variables x range over strings over the given alphabet,
denotes the empty string, *a*(w) denotes the string *a*w, and
f_{q}(x,y) indicates that M, when given input w, can reach a
configuration with state q, in which xy is on the tape, with x in
reverse order, and the head of M points at the first position of y.
Under this interpretation f_{q0}(,w) is certainly a
true formula, as the initial configuration is surely reachable. Here
q0 is the initial state, and w is a representation of w made from the
constant and function symbols of the logic. Furthermore the formula
x y: f_{q-acc}(x,y) with q-acc the
acceptance state, holds iff M accepts w.

Whenever M has a transition from state q to state r, reading a, writing b, and moving right, the formula

x
y:
f_{q}(x,ay) => f_{r}(bx,y)

x
y:
f_{q}(cx,ay) => f_{r}(x,cby)

x
y:
f_{q}(,ay) =>
f_{r}(,by),

x
y:
f_{q}(x,) =>
f_{r}(bx,)

x
y:
f_{q}(cx,) =>
f_{r}(x,cb)

x
y:
f_{q}(,) => f_{r}(,b).

f_{q0}(,w) & T =>
x
y:
f_{q-acc}(x,y).

Thus, in order to decide whether or not M accepts w, it suffices to check whether or not the formula above is a theorem of first order logic.

Rob van Glabbeek | rvg@cs.stanford.edu |