Formal SyntaxEdit
In The Predicate Language, we informally described our sentential language. Here we give its formal syntax or grammar. We will call our language . This is an expansion of the sentential language and will include as a subset.
VocabularyEdit
 Variables: Lower case letters 'n'–'z' with a natural number subscript. Thus the variables are:
 Operation letters: Lower case letters 'a'–'m' with (1) a natural number superscript and (2) a natural number subscript.
 A constant symbol is a zeroplace 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.
 A sentence letter is a zeroplace predicate letter.
 Sentential connectives:
 Quantifiers:
 Grouping symbols:
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 zeroplace predicate letters, namely predicate letters with the superscript '0'. The vocabulary of , the sentential logic formal language, includes zeroplace predicate letters, sentential connectives, and grouping symbols.
ExpressionsEdit
Any string of symbols from is an expression. Not all expressions are grammatically well formed. The primary wellformed expression is a formula. However, there are also well formed entities that are smaller than formulae, namely quantifier phrases and terms.
Formation rulesEdit
Quantifier phrasesEdit
A quantifier phrase is a quantifier followed by a variable. The following are examples:
TermsEdit
An expression of is a term of if and only if it is constructed according to the following rules.
 i. A variable is a term.
 ii. A constant symbol (zeroplace operation letter, i.e., an operation letter with the superscript '0') is a term.
 iii. If is an nplace operation letter (n greater than 0) and are terms, then

 is a term.
A name is a term with no variables.
FormulaeEdit
An expression of is a wellformed formula of if and only if it is constructed according to the following rules.
 i. A sentence letter (a zeroplace predicate letter) is a wellformed formula.
 ii. If is an nplace predicate letter (n greater than 0) and are terms, then

 is a wellformed formula.
 iii. If and are wellformed formulae, then so are each of:
 iv. If is a wellformed formula and is a variable, then each of the following is a wellformed formula:
In general, we will use 'formula' as shorthand for 'wellformed formula'. We will see in the section Free and Bound Variables that only some formulae are sentences.
Additional terminologyEdit
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 zeroplace 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 zeroplace operation letters, and some prefer to avoid the word altogether.)
A sentence letter is a zeroplace predicate letter.
The universal quantifier is the symbol . The existential quantifier is the symbol .
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 a 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 nonprime 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 ). However, there is a change as we move to . 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.
ExamplesEdit
By clause (i) in the definition of 'term', and are terms. Similarly, , , and 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.
Then, by clause (iii) of the definition of 'term', the following is a term.
Finally, (1) is a term by clause (iii) of the definition of 'term'. However, because it contains variables, it is not a name.
We already saw that (1) is a term. Thus, by clase (ii) of the definition of formula, (2) is a formula.
By clause (i) in the definition of 'term', , , and are terms.
By clause (ii) of the definition for 'formula', the following are formulae.
By clause (iiid) of the definition for 'formula', the following is a formula.
By clause (iva) of the definition for 'formula', the following is a formula.
By clause (iiib) of the definition for 'formula', the following is a formula.
Finally, by clause (ivb) of the definition for 'formula', (3) is a formula.