4  wffs in FOL

The rules for wffs in FOL, or for the construction of a wff\(_{\text{FOL}}\), have three components:

Collectively, these rules will tell us how to use each of our various symbol types from the FOL alphabet:

4.1 Predicates in FOL

Upper-case letters in FOL are predicates, and predicates have arities. The arity of a predicate is the number of terms that must follow it. In practice, the arity of a predicate is inferred from the use of a predicate. In theoretical contexts, as in the definition of atomic formulas below, it may be important to make the arity explicit by appending a numerical (or variable) superscript. f ## Terms in FOL

One of the differences between the alphabets of SL and FOL is the use in FOL of lower-case letters. Collectively, we will call lower-case letters terms. We distinguish between two subsets of these, purely syntactically, as follows:

  • constants are lower-case letters \(a \ldots w\), with or without numerical subscripts
  • variables are \(x, y,\) and \(z\), with or without numerical subscripts

In formal or meta-theoretical contexts, we represent terms, constants, and variables, respectively, with the following Greek letters:

  • \(\tau\): term
  • \(\gamma\): constant
  • \(\chi\): variable

4.2 Atomic formulas in FOL

We define atomic formulas in FOL as follows:

For predicate \(\Pi^n\) and terms \(\langle \tau_1 \ldots \tau_n \rangle\), \(\Pi^n\langle \tau_1 \ldots \tau_n\rangle\) is an atomic formula in FOL.

As our first rule, we allow that such formulas are well-formed:

  1. An atomic formula in FOL is a wff\(_{\text{FOL}}\)

4.3 Compound formulas in FOL

Two subsets of recursive rules define the use of logical connectives, quantifiers, and variables in FOL (and parentheses by implication).

4.3.1 Logical connectives in FOL

The first set are identical to the next five rules in SL:

  1. If \(\phi\) is a wff\(_{\text{FOL}}\), \(\neg \phi\) is a wff\(_{\text{FOL}}\)
  2. If \(\phi\) is a wff\(_{\text{FOL}}\) and \(\psi\) is a wff\(_{\text{FOL}}\), \((\phi \vee \psi)\) is a wff\(_{\text{FOL}}\)
  3. If \(\phi\) is a wff\(_{\text{FOL}}\) and \(\psi\) is a wff\(_{\text{FOL}}\), \((\phi \wedge \psi)\) is a wff\(_{\text{FOL}}\)
  4. If \(\phi\) is a wff\(_{\text{FOL}}\) and \(\psi\) is a wff\(_{\text{FOL}}\), \((\phi \to \psi)\) is a wff\(_{\text{FOL}}\)
  5. If \(\phi\) is a wff\(_{\text{FOL}}\) and \(\psi\) is a wff\(_{\text{FOL}}\), \((\phi \leftrightarrow \psi)\) is a wff\(_{\text{FOL}}\)

4.3.2 Quantifiers and variables in FOL

The second pair define well-formedness for the use of quantifiers and variables:

  1. If \(\phi\) is a wwff\(_{\text{FOL}}\), \(\forall \chi \phi\) is a wff\(_{\text{FOL}}\)
  2. If \(\phi\) is a wwff\(_{\text{FOL}}\), \(\exists \chi \phi\) is a wff\(_{\text{FOL}}\)

4.4 Final rule

And, finally, we stipulate that no other ‘formulas’ (that is, strings of symbols in the alphabet of FOL) are wffs\({_\text{FOL}}\).

  1. No other formula is a wff\({_\text{FOL}}\)

4.5 The complete set

  1. An atomic formula in FOL is a wff\(_{\text{FOL}}\)
  2. If \(\phi\) is a wff\(_{\text{FOL}}\), \(\neg \phi\) is a wff\(_{\text{FOL}}\)
  3. If \(\phi\) is a wff\(_{\text{FOL}}\) and \(\psi\) is a wff\(_{\text{FOL}}\), \((\phi \vee \psi)\) is a wff\(_{\text{FOL}}\)
  4. If \(\phi\) is a wff\(_{\text{FOL}}\) and \(\psi\) is a wff\(_{\text{FOL}}\), \((\phi \wedge \psi)\) is a wff\(_{\text{FOL}}\)
  5. If \(\phi\) is a wff\(_{\text{FOL}}\) and \(\psi\) is a wff\(_{\text{FOL}}\), \((\phi \to \psi)\) is a wff\(_{\text{FOL}}\)
  6. If \(\phi\) is a wff\(_{\text{FOL}}\) and \(\psi\) is a wff\(_{\text{FOL}}\), \((\phi \leftrightarrow \psi)\) is a wff\(_{\text{FOL}}\)
  7. If \(\phi\) is a wwff\(_{\text{FOL}}\), \(\forall \chi \phi\) is a wff\(_{\text{FOL}}\)
  8. If \(\phi\) is a wwff\(_{\text{FOL}}\), \(\exists \chi \phi\) is a wff\(_{\text{FOL}}\)
  9. No other formula is a wff\({_\text{FOL}}\)