**Go backward to** 2.3.2 Logical Connectives

**Go up to** 2.3 Axioms

**Go forward to** 2.3.4 Terms

### 2.3.3 Atomic Formulae

ATOM ::= TRUTH | PREDICATION | DEFINEDNESS
| EXISTL-EQUATION | STRONG-EQUATION

An *atomic formula* `ATOM` is well-formed (with respect to
the local environment and variable declarations) if it is well-sorted
and expands to a unique atomic formula for constructing sentences.
The notions of when an atomic formula is *well-sorted*, of
when a term is *well-sorted for a particular sort*, and of the
*expansions* of atomic formulae and terms, are indicated
below for the various constructs.

Due to overloading of predicate and/or operation symbols, a
well-sorted atomic formula or term may have several expansions,
preventing it from being well-formed. Qualifications on operation and
predicate symbols may be used to determine the intended expansion and
make it well-formed; explicit sorts on arguments and/or results may
also help to avoid unintended expansions.

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk