Language

The language in First-Order Predicate Logic
is specified by a disjoint pair of sets:
the set of operation symbols
the set of predicate symbols
and an arity function

The language consists of the following:

Variables

This is a countably infinite set disjoint from and
We denote variables by or

Terms

Or -terms are defined inductively:

1. Every variable is a term
2. if with and are terms then is a term

Atomic formulae

Two kinds:

1. If , are terms then is an atomic formulae
2. if with and are terms then is an atomic formulae.

Formulae

1. Atomic formulae are formulae
2. is a formula
3. If , are formulae then so is
4. If is a formula and is a Free Variable in then is a formula