The well-formed terms and propositions of ordinary
first-order logic have the following
syntax:
Terms: • t \equiv c \mid x \mid f (t_{1},\dotsc, t_{n}), that is, a term is
recursively defined to be a constant
c (a named object from the
domain of discourse), or a variable
x (ranging over the objects in the domain of discourse), or an
n-ary function
f whose arguments are terms
tk. Functions map
tuples of objects to objects. Propositions: • A, B, ... \equiv P (t_{1},\dotsc, t_{n}) \mid A \wedge B \mid \top \mid A \vee B \mid \bot \mid A \supset B \mid \forall x.\ A \mid \exists x.\ A , that is, a proposition is recursively defined to be an
n-ary
predicate P whose arguments are terms
tk, or an expression composed of
logical connectives (and, or) and
quantifiers (for-all, there-exists) used with other propositions. An
atomic formula or
atom is simply a predicate applied to a tuple of terms; that is, an atomic formula is a formula of the form
P (
t1 ,…,
tn) for
P a predicate, and the
tn terms. All other well-formed formulas are obtained by composing atoms with logical connectives and quantifiers. For example, the formula ∀
x. P (
x) ∧ ∃
y. Q (
y,
f (
x)) ∨ ∃
z. R (
z) contains the atoms • P (x) • Q (y, f (x)) • R (z). As there are no quantifiers appearing in an atomic formula, all occurrences of variable symbols in an atomic formula are free. ==See also==