Formulas

Here is Leary's Definition 1.3.3 (p. 13) for formulas. (Note: we will later distinguish between two kinds of formulas, sentences and non-sentences. Both are sentence-like; the only difference is that the non-sentences contain free variables, i.e. variables unbound by a quantifier. Thus they don't "express a complete thought," to revert to the definition of a sentence I learned in middle school English.

Definition: If $\mathcal{L}$ is a first-order language, a formula of $\mathcal{L}$ is a nonempty finite string $\phi$ of symbols from $\mathcal{L}$ such that either:

1. $\phi$ is $=t_1t_2$, where $t_1$ and $t_2$ are terms of $\mathcal{L}$, or
2. $\phi$ is $Rt_1t_2\ldots t_n$, where $R$ is an $n$-ary relation symbol of $\mathcal{L}$ and $t_1, t_2, \ldots, t_3$ are all terms of $\mathcal{L}$, or
3. $\phi$ is $(\neg \alpha)$, where $\alpha$ is a formula of $\mathcal{L}$, or
4. $\phi$ is $(\alpha \vee \beta)$, where $\alpha$ and $\beta$ are formulas of $\mathcal{L}$, or
5. $\phi$ is $(\forall v)(\alpha)$, where $v$ is a variable and $\alpha$ is a formula of $\mathcal{L}$.

There are a few minor points to make here. The first clause states that $=t_2t_2$ is a term. This looks weird, but it is just an instance of the official syntax of our language. '$=$' is a special instance of a two-place relation symbol, and like the other binary relation symbols (as treated in the next clause), it yields a formula when it is followed by two terms. Of course, we would ordinarily write this using infix notation rather than prefix notation, as '$t_1 = t_2$'.

Another point to notice is that the official language requires parentheses around every compound formula. (The atomic formulas are those defined by clauses 1 and 2; the rest are nonatomic or compound. Any formula constructed out of other formulas together with a connective or a quantifier is compound.) This is different than the convention in Barwise and Etchemendy, but it makes things simpler. Informally, we can drop some of these parentheses, e.g. the outermost parentheses, as long as this does not hurt readability or introduce ambiguity.