Skip to content

2.1 Terms, Predicates, Formulas

Syntax of first order logic including terms, predicate symbols, and the formation of formulas.

First order logic extends propositional logic by introducing internal structure inside statements, so that instead of treating statements as atomic objects, we can describe objects, properties of objects, and relations between objects in a precise formal language.

Symbols and Signatures

To define the language, we begin with a collection of symbols that describe the kinds of objects and operations that are allowed, and this collection is called a signature.

A signature consists of the following components.

A set of constant symbols:

c,d,e, c, d, e, \dots

which are intended to name specific objects.

A set of function symbols, each with a fixed arity. For example:

f,g,h, f, g, h, \dots

where a symbol of arity nn takes nn arguments.

A set of predicate symbols, each with a fixed arity. For example:

P,Q,R, P, Q, R, \dots

where a predicate symbol of arity nn expresses a property or relation involving nn objects.

In addition, the language includes logical symbols such as:

¬,,,,,, ¬, \land, \lor, \to, \leftrightarrow, \forall, \exists

together with variables:

x,y,z,x1,x2, x, y, z, x_1, x_2, \dots

These symbols together form the alphabet of first order logic.

Definition 2.1 (Terms)

Terms are expressions that denote objects, and they are defined inductively.

Every variable is a term.

Every constant symbol is a term.

If ff is a function symbol of arity nn, and t1,t2,,tnt_1, t_2, \dots, t_n are terms, then:

f(t1,t2,,tn) f(t_1, t_2, \dots, t_n)

is a term.

No other expressions are terms.

This definition ensures that terms are built in a finite number of steps from variables and constants using function symbols.

Example 2.2

The following are terms:

x x

c c

f(x) f(x)

g(x,y) g(x, y)

f(g(x),h(y,c)) f(g(x), h(y, c))

Each term is constructed by repeatedly applying function symbols to previously constructed terms.

Definition 2.3 (Atomic Formulas)

Atomic formulas express basic statements about objects.

If PP is a predicate symbol of arity nn, and t1,t2,,tnt_1, t_2, \dots, t_n are terms, then:

P(t1,t2,,tn) P(t_1, t_2, \dots, t_n)

is an atomic formula.

In addition, equality is treated as a special binary predicate, so for any terms t1t_1 and t2t_2:

t1=t2 t_1 = t_2

is an atomic formula.

Atomic formulas are the simplest formulas in first order logic, and they correspond to statements about objects and their relationships.

Example 2.4

The following are atomic formulas:

P(x) P(x)

Q(x,y) Q(x, y)

R(f(x),g(y)) R(f(x), g(y))

x=y x = y

f(x)=g(y) f(x) = g(y)

Each of these expresses a property or relation involving the given terms.

Definition 2.5 (Formulas)

The set of formulas is defined inductively.

Every atomic formula is a formula.

If AA is a formula, then:

¬A ¬A

is a formula.

If AA and BB are formulas, then:

(AB),(AB),(AB),(AB) (A \land B), \quad (A \lor B), \quad (A \to B), \quad (A \leftrightarrow B)

are formulas.

If AA is a formula and xx is a variable, then:

xA \forall x \, A

and:

xA \exists x \, A

are formulas.

No other expressions are formulas.

This definition extends propositional formulas by allowing quantifiers, which bind variables and express generality or existence.

Example 2.6

The following are formulas:

P(x) P(x)

¬P(x) ¬P(x)

P(x)Q(y) P(x) \land Q(y)

xP(x) \forall x \, P(x)

yQ(y) \exists y \, Q(y)

x(P(x)Q(x)) \forall x \, (P(x) \to Q(x))

x(P(x)¬Q(x)) \exists x \, (P(x) \land ¬Q(x))

Each formula is built from atomic formulas using logical connectives and quantifiers.

Free and Bound Variables

Variables in a formula may occur either freely or bound by quantifiers, and this distinction is essential for understanding the meaning of formulas.

A variable is bound if it occurs within the scope of a quantifier that refers to that variable.

A variable is free if it is not bound by any quantifier.

For example, in:

xP(x,y) \forall x \, P(x, y)

the variable xx is bound, while yy is free.

In:

y(P(x,y)Q(y)) \exists y \, (P(x, y) \land Q(y))

the variable yy is bound, while xx is free.

Definition 2.7 (Closed Formula)

A formula is closed if it has no free variables.

Closed formulas are also called sentences.

For example:

xP(x) \forall x \, P(x)

is closed, while:

P(x) P(x)

is not closed.

Closed formulas are important because they can be assigned a definite truth value in a structure, whereas formulas with free variables depend on assignments of values to those variables.

Substitution

Given a formula AA, a variable xx, and a term tt, one may form a new expression A[x:=t]A[x := t] by replacing occurrences of xx by tt.

However, care must be taken to avoid variable capture, which occurs when a free variable becomes bound after substitution.

For example, in:

xP(x,y) \forall x \, P(x, y)

replacing yy by xx would produce:

xP(x,x) \forall x \, P(x, x)

and here the new occurrence of xx is bound, which changes the meaning of the formula.

To avoid such problems, substitutions must be defined carefully, often by renaming bound variables before performing the replacement.

Lemma 2.8 (Unique Readability)

Every term and every formula admits a unique decomposition according to the formation rules.

Proof

The proof follows the same pattern as in propositional logic and proceeds by induction on the construction of terms and formulas.

Each term is either a variable, a constant, or of the form f(t1,,tn)f(t_1, \dots, t_n), and these cases are disjoint and uniquely determined.

Each formula is either atomic, a negation, a binary combination of formulas, or a quantified formula, and again the formation rules ensure that these cases are disjoint and uniquely determined.

Therefore every expression has a unique syntactic structure.

Structural Induction

The inductive definitions of terms and formulas give rise to principles of structural induction.

To prove a property for all terms, it is enough to prove it for variables and constants and to show that it is preserved under the application of function symbols.

To prove a property for all formulas, it is enough to prove it for atomic formulas and to show that it is preserved under logical connectives and quantifiers.

These principles allow one to reason rigorously about all expressions in the language.