Formula Glossary
Definition
A formula is the abstract form of a sentence. The grammar defining the syntax of first order formulae reads as follows:
 A term is the result of applying an nary function symbol to n terms;
 An atom is the result of applying an nary predicate symbol to n terms;
 Every atom is a formula;
 If A is a formula, NOTA is a formula;
 If A and B are formulae, all of A AND B, A OR B, A IMP B and A IFF B are formulae;
 If A is a formula containing a name m and v is a variable not occurring in A, both ALLvA^{v}_{m}and SOMEvA^{v}_{m}are formulae.
 Nothing is a formula except as a consequence of 1 – 6 above.
Comments
Function and predicate symbols have not been defined here. Nor have variables. In the version of the language we use for proofs, they are all single letters, though in Logic for Fun they can be longer strings. It is important to note that the case n = 0 is included, so the basic terms are names.
The above definition is for the language with unrestricted quantifiers. Adding restricted quantifiers quantifiers is not hard, but here we illustrate with the simpler version.
For purely propositional logic, simply omit clause 6. Since the constituent parts of atoms play no role in propositional logic, atoms behave just like 0ary predicates, so we normally write them as such (i.e. as p, q, r, etc.).
Parentheses have not been mentioned above. On this definition, a formula is a rather abstract object—a kind of tree. When we want to write it as a linear string of symbols, we may put in parentheses wherever they are useful to resolve ambiguities or to make it clearer for the reader.
Examples
 f(a,g(b)) is a term, because a and b are names (0ary function symbols applied to zero arguments) and therefore terms, and g(b) is the result of applying the unary function symbol 'g' to one term.

SOMEx
(F(f(a,g(x)))
IMP NOTALLy Gy) is
a formula, because it results by substituting
variable x for name b
in F(f(a,g(b))
IMP NOTALLy Gy and
applying clause 6 of the recursive definition.
In turn, F(f(a,g(b)) IMP NOTALLy Gy is a formula because it is the result of applying a binary connective to the two shorter formulae F(f(a,g(b)) and NOTALLy Gy.
F(f(a,g(b)) is an atom, and therefore a formula, got by applying the unary predicate symbol F to a term.
NOTALLy Gy comes by clause 4 of the definition of a formula, given that ALLy Gy is a formula, which it is because it is the result of applying the quantifier ALLy to Ga^{y}_{a} and because Ga is an atom.