# Formal Syntax

In The Predicate Language, we informally described our sentential language. Here we give its formal syntax or grammar. We will call our language ${\mathcal {L_{P}}}\,\!$. This is an expansion of the sentential language ${\mathcal {L_{S}}}\,\!$ and will include ${\mathcal {L_{S}}}\,\!$ as a subset.

## Vocabulary

* Variables: Lower case letters 'n'–'z' with a natural number subscript. Thus the variables are:
       $n_{0},\ n_{1},\ ...,\ o_{0},\ o_{1},\ ...,\ ...,\ z_{0},\ z_{1},\ ...\,\!$
* Operation letters: Lower case letters 'a'–'m' with (1) a natural number superscript and (2) a natural number subscript.
       $a_{0}^{0},\ a_{1}^{0},\ ...,\ b_{0}^{0},\ b_{1}^{0},\ ...,\ ...,\ m_{0}^{0},\ m_{1}^{0},\ ...\,\!$
       $a_{0}^{1},\ a_{1}^{1},\ ...,\ b_{0}^{1},\ b_{1}^{1},\ ...,\ ...,\ m_{0}^{1},\ m_{1}^{1},\ ...\,\!$
    A constant symbol is a zero-place operation letter. This piece of terminology is not completely standard.
* Predicate letters: Upper case letters 'A'–'Z' with (1) a natural number superscript and (2) a natural number subscript.
       $\mathrm {A_{0}^{0}} ,\ \mathrm {A_{1}^{0}} ,\ ...,\ \mathrm {B_{0}^{0}} ,\ \mathrm {B_{1}^{0}} ,\ ...,\ ...,\ \mathrm {Z_{0}^{0}} ,\ \mathrm {Z_{1}^{0}} ,\ ...\,\!$
       $\mathrm {A_{0}^{1}} ,\ \mathrm {A_{1}^{1}} ,\ ...,\ \mathrm {B_{0}^{1}} ,\ \mathrm {B_{1}^{1}} ,\ ...,\ ...,\ \mathrm {Z_{0}^{1}} ,\ \mathrm {Z_{1}^{1}} ,\ ...\,\!$
    A sentence letter is a zero-place predicate letter.
* Sentential connectives:
       $\land ,\ \lor ,\ \lnot ,\ \rightarrow ,\ \leftrightarrow \,\!$
* Quantifiers:
       $\forall ,\ {\mbox{and}}\ \exists ,\!$
* Grouping symbols:
       $(\ {\mbox{and}}\ )\,\!$
The superscripts on operation letters and predicate letters indicate the number of places and are important for formation rules. The subscripts on variables, operation letters, and predicate letters are to ensure an infinite supply of symbols in these classes. On a subsequent page we will abbreviate away most superscript use by letting the context make the number of places clear. We will also abbreviate away most subscript use by letting a symbol without a subscript abbreviate one with the subscript '0'. For now, though, we stick with the unabbreviated form.
The sentence letters of sentential logic are zero-place predicate letters, namely, predicate letters with the superscript '0'. The vocabulary of ${\mathcal {L_{S}}}\,\!$, the sentential logic formal language, includes zero-place predicate letters, sentential connectives, and grouping symbols.

## Expressions

Any string of symbols from ${\mathcal {L_{P}}}\,\!$ is an expression. Not all expressions are grammatically well-formed. The primary well-formed expression is a formula. However, there are also well-formed entities that are smaller than formulae, namely quantifier phrases and terms.

## Formation rules
### Quantifier phrases

A quantifier phrase is a quantifier followed by a variable. The following are examples:
    $\forall x_{0}\,\!$
    $\exists y_{37}\,\!$

### Terms

An expression of ${\mathcal {L_{P}}}\,\!$ is a term of ${\mathcal {L_{P}}}\,\!$ if and only if it is constructed according to the following rules.
    $\,{\mbox{ i.}}$ A variable is a term.
    ${\mbox{ ii.}}$ A constant symbol (zero-place operation letter, i.e., an operation letter with the superscript '0') is a term.
    ${\mbox{iii.}}$ If $\zeta \,\!$ is an n-place operation letter (n greater than 0) and $\alpha _{1},\ \alpha _{2},\ ...,\ \alpha _{n}\,\!$ are terms, then
          $\zeta (\alpha _{1},\alpha _{2},...,\alpha _{n})\,\!$
       is a term.
A name is a term with no variables.

### Formulae

An expression of ${\mathcal {L_{P}}}\,\!$ is a well-formed formula of ${\mathcal {L_{P}}}\,\!$ if and only if it is constructed according to the following rules.
    $\,{\mbox{ i.}}$ A sentence letter (a zero-place predicate letter) is a well-formed formula.
    ${\mbox{ ii.}}$ If $\pi \,\!$ is an n-place predicate letter (n greater than 0) and $\alpha _{1},\ \alpha _{2},\ ...,\ \alpha _{n}\,\!$ are terms, then
          $\pi (\alpha _{1},\alpha _{2},...,\alpha _{n})\,\!$
    is a well-formed formula.
    ${\mbox{iii.}}$ If $\varphi \,\!$ and $\psi \,\!$ are well-formed formulae, then so are each of:
       ${\mbox{iii-a.}}\ \ \lnot \varphi \,\!$
       ${\mbox{iii-b.}}\ \ (\varphi \land \psi )\,\!$
       ${\mbox{iii-c.}}\ \ (\varphi \lor \psi )\,\!$
       ${\mbox{iii-d.}}\ \ (\varphi \rightarrow \psi )\,\!$
       ${\mbox{iii-e.}}\ \ (\varphi \leftrightarrow \psi )\,\!$
    ${\mbox{ iv.}}$ If $\varphi \,\!$ is a well-formed formula and $\alpha \,\!$ is a variable, then each of the following is a well-formed formula:
       ${\mbox{iv-a.}}\ \ \forall \alpha \,\varphi \,\!$
       ${\mbox{iv-b.}}\ \ \exists \alpha \,\varphi \,\!$
In general, we will use 'formula' as shorthand for 'well-formed formula'. We will see in the section Free and Bound Variables that only some formulae are sentences.

## Additional terminology

A few of these terms are repeated from above. All definitions from the sentential logic additional terminology section apply here except the definitions of 'atomic formula' and 'molecular formula'. These latter two terms are redefined below.
A constant symbol is a zero-place operation letter. (Note that different authors will vary on this.)
A name is a term in which no variables occur. (Note that different authors will vary on this. Some use 'name' only for zero-place operation letters, and some prefer to avoid the word altogether.)
A sentence letter is a zero-place predicate letter.
The universal quantifier is the symbol $\forall \,\!$. The existential quantifier is the symbol $\exists \,\!$.
A quantified formula is a formula that begins with a left parenthesis followed by a quantifier. A universal generalization is a formula that begins with a left parenthesis followed by a universal quantifier. An existential generalization is a formula that begins with a left parenthesis followed by an existential quantifier.
An atomic formula is one formed solely by formula formation clause {i} or {ii}. Put another way, an atomic formula is one in which no sentential connectives or quantifiers occur. A molecular formula is one that is not atomic. Thus a molecular formula has at least one occurrence of either a sentential connective or a quantifier. (Revised from sentential logic.)
A prime formula is a formula that is either an atomic formula or a quantified formula. A non-prime formula is one that is not prime. (Note that this is not entirely standard terminology. It has been used this way by some authors, but not often.)
The main operator of a molecular formula is the last occurrence of a sentential connective or quantifier added when the formula was constructed according to the rules above. If the main operator is a sentential connective, then it is also called the 'main connective' (as was done in the sentential language ${\mathcal {L_{S}}}\,\!$). However, there is a change as we move to ${\mathcal {L_{P}}}\,\!$. In predicate logic, it is no longer true that all molecular formulae have a main connective. Some main operators are now quantifiers rather than sentential connectives.

## Examples
#### Example 1

    $(1)\quad f_{0}^{2}(g_{2}^{2}(x_{0},f_{0}^{2}(a_{0}^{0},c_{2}^{0})),f_{0}^{2}(b_{0}^{0},y_{3}))\,\!$
By clause (i) in the definition of 'term', $x_{0}\,\!$ and $y_{3}\,\!$ are terms. Similarly, $a_{0}^{0}\,\!$, $b_{0}^{0}\,\!$, and $c_{2}^{0}\,\!$ are terms by clause (ii) of the definition of 'term'.
Next, by clause (iii) of the definition of 'term', the following two expressions are terms.
    $f_{0}^{2}(a_{0}^{0},c_{2}^{0})\,\!$
    $f_{0}^{2}(b_{0}^{0},y_{3})\,\!$
Then, by clause (iii) of the definition of 'term', the following is a term.
    $g_{2}^{2}(x_{0},f_{0}^{2}(a_{0}^{0},c_{2}^{0}))\,\!$
Finally, (1) is a term by clause (iii) of the definition of 'term'. However, because it contains variables, it is not a name.

#### Example 2

    $(2)\quad \mathrm {F_{0}^{1}} (f_{0}^{2}(g_{2}^{2}(x_{0},f_{0}^{2}(a_{0}^{0},c_{2}^{0})),f_{0}^{2}(b_{0}^{0},y_{3})))\,\!$
We already saw that (1) is a term. Thus, by clause (ii) of the definition of formula, (2) is a formula.

#### Example 3

    $(3)\quad \exists y_{0}\,(\forall x_{0}\,(\mathrm {F_{0}^{2}} (x_{0},y_{0})\rightarrow \mathrm {G_{0}^{2}} (x_{0},z_{0}))\land \mathrm {H_{0}^{1}} (y_{0}))\,\!$
By clause (i) in the definition of 'term', $x_{0}\,\!$, $y_{0}\,\!$, and $z_{0}\,\!$ are terms.
By clause (ii) of the definition for 'formula', the following are formulae.
    $\mathrm {F_{0}^{2}} (x_{0},y_{0})\,\!$
    $\mathrm {G_{0}^{2}} (x_{0},z_{0})\,\!$
    $\mathrm {H_{0}^{1}} (y_{0})\,\!$
By clause (iii-d) of the definition for 'formula', the following is a formula.
    $(\mathrm {F_{0}^{2}} (x_{0},y_{0})\rightarrow \mathrm {G_{0}^{2}} (x_{0},z_{0}))\,\!$
By clause (iv-a) of the definition for 'formula', the following is a formula.
    $\forall x_{0}\,(\mathrm {F_{0}^{2}} (x_{0},y_{0})\rightarrow \mathrm {G_{0}^{2}} (x_{0},z_{0}))\,\!$
By clause (iii-b) of the definition for 'formula', the following is a formula.
    $(\forall x_{0}\,(\mathrm {F_{0}^{2}} (x_{0},y_{0})\rightarrow \mathrm {G_{0}^{2}} (x_{0},z_{0}))\land \mathrm {H_{0}^{1}} (y_{0}))\,\!$
Finally, by clause (iv-b) of the definition for 'formula', (3) is a formula.