formula (thing)

(logic, mathematics:)
(Logic). A formula is a wff¹ with at least one free variable. As such, it may be impossible to assign a truth value to it, since the value depends on the assignments to the free variables.

These are all formulae (in the language of arithmetic):

xⁿ+yⁿ=zⁿ

`x', `y', `z' and `n' occur free. In arithmetic, we now know that there are no true assignments when n>2; there are infinitely many true assignments for n=1 and n=2.

∀x:y=x*x

`y' occurs free. This particular formula is always false (in arithmetic), since for any given value there is at most one `x' for which y=x*x. For instance, if y=36, it is not true that `∀x:36=x*x'.

∀x:~∃y:x*y=z

`z' occurs free. In arithmetic, the formula may be translated as saying "z is prime".

The last example shows how every formula defines a predicate. Hence their importance: a formula can be seen as a definition of some concept.

(Mathematics). Formulae in mathematics are based on formulae in logic. The usage is less rigid, of course. Generally, no quantifiers are involved in a mathematical formula:

E=m*c²

Strictly speaking, this defines a relation on 3 free variables `E',`m',`c'. In practice, we use it to derive the "correct" value of one variable from the other 2.

x=y²

This formula defines `x' in terms of `y'. However, it doesn't quite define `y' in terms of `x', due to a small problem with signs

When there exists a unique solution to one free variable given the values of the other free variables, we may think of the formula not as a predicate, but as a computational method for computing the final variable.

In Physics and Engineering, variables come with dimensions. Dimensional analysis checks that the dimensions involved in a formula are consistent. Thus physicists and engineers talk about "dimensionally incorrect formulae": they cannot be correct, ever, because the dimensions on both sides of the equality are not the same.

Footnotes:

1. Yes, "wff" does incorporate the term "formula" in it, but it is usually defined first, and "formula" in terms of it. Think of "wff" as what linguists call an "utterance".
2. The converse is generally not true; for instance, there are 2^ℵ₀ predicates on the natural numbers and only ℵ₀ formulae in the language of arithmetic!).