Im reading the book Logic, Mathematics and Computer Science by Yves Nievergelt, and in the second chapter when defining the well-formed formulae the author gives the following definition:
Definition (well-formed formulae). Select Select three disjoint lists of symbols. Every symbol from the first list of symbols, which may consist of one or more letter(s) from a specified alphabet, $P, Q...$, is called a formulaic letter. Such formulaic letters are not parts of the predicate calculus, but they help in describing the following rules to define well-formed formulae.
Also, every symbol from the second list of symbols, which may consist of one or more letter(s) from a specified alphabet, $A, B, ...$, is called a propositional variable or sentence symbol. (Propositional variables may later be replaced in pure calculi by functional or relational variables, or in applied calculi by atomic formulae, which may include individual variables or constants specific to applications.)
Moreover, every symbol from the third list of symbols, which may consist of one or more letter(s) from a specified alphabet, $X, Y, ...$, is called an individual variable.(Individual variables may later be replaced by items specific to applications, for instance, numbers in arithmetic, or points in geometry.)
Every propositional variable or atomic formula is a well-formed formula. For all well-formed formulae $P$ and $Q$, and for every individual variable X, the following four strings of symbols are also well-formed formulae:
- $\lnot (P)$
- $(P) \Rightarrow (Q)$
- $\forall X(P)$
- $\exists X(P)$
Furthermore, only strings of symbols built from letters or variables through appli- cations of the rules W1–W4 can be well-formed formulae.
I got confused because the author dont used any symbol from the second list $A, B, ...$, Its not clear for me what the propositional variable really means in this description, but I think I need to understand it properly before proceed since he says that every propositional variable is a well-formed formula, I guess that the formulaic letters from the first list represent formulas which are constructed from propositional variables and that the propositional can but need not to contain individual variables.
I want to understand what the author really means by propositional variables/sentence symbols, and if there is a more clear way to define well-formed formulas for predicate calculus, also any tip on study of first-order logic will be appreciated.
What the author calls formulaic letters [$P,Q$] are usually called "metavariables": they are not part of the formal language but they are used in the text to name formulas ("formulaic letters are not parts of the predicate calculus, but they help in describing the following rules to define well-formed formulae.").
See a different example of definition of formula:
Here $x=y$ is an expression of the formal language, while $\varphi$ and $\psi$ are metavariables ("formulaic letters").
Individual variables [$X,Y$] are variables naming objects of the domain of discourse (more usually not capital letters), like in set theory: $x \in y$ (see Examples page 82).
Thus, considering examples from set theory, we have that $x \in y$ is an atomic formula and that $\lnot (x \in y)$ and $(x \in y) \lor (x \in z)$ and $\exists x \forall y \lnot (x \in y)$ are examples of formulas.
In some cases, it is useful to consider as part of the language, not only atomic formulas, like $x=y$ and $x \in y$, but also propositional variables (or sentence symbols, aka: $0$-ary predicate symbols).
When we will fix an interpretation $\mathfrak I$, a sentence symbol $A$ will be interpreted as a truth value.