First-order logic is a formal language, which means that it has both an alphabet and rules for constructing valid expressions, or formulas, in the language. The language consists of the following:

• Terms, including both variables (x, y, z, ...) and names (a, b, c, ...) (Subscripts are used with both variables and names to make an infinite number of them available)
• Predicates: F^j, G^k, H^m, where the lower-case letter is a number that indicates how many terms are included in the predicate (These are referred to as n-ary predicates and subscripts can be used when needed)
• Punctuation: (, )
• Connectives, including the unary connective ~ and the binary connectives (Read "... and ...."), ∨ ("... or ...."), ("If ..., then ...."), and ("... if and only if ....")
• Quantifiers: ∀ ("For all ..."), ∃ ("There exists ...") (Quantifiers must be followed by a variable)

There are only five rules for creating formulas:

• 1. An n-ary predicate followed...