construction of well-formed formulas

Given a countable set $V$ of propositional variables, and a set $F$ of logical connectives disjoint from $V$, one can create the set of all finite strings (or words) over $V\cup F$.

Ways of Forming a Single Well-formed Formula

A well-formed formula, or wff for short, is then a special kind of finite string, sometimes called a term, formed in a specific, pre-determined manner:

1. First, any propositional variable is always a wff. A wff that is a propositional variable is sometimes called an atom.

2. Once we have formed a set wffs, we may form new ones. Given an $n$-ary connective $\alpha \in F$, and wffs $p_1,\mathrm{\dots },p_n$, there are several methods to represent the newly formed wff, some of the common ones are:

   • $\alpha p_1\mathrm{\cdots }{p}_n$

   • $p_1\mathrm{\cdots }{p}_n\alpha$

   • $(\alpha p_1\mathrm{\cdots }{p}_n)$

   • $\alpha (p_1,\mathrm{\cdots },p_n)$

   In particular, every nullary connective (constant) is a wff (with no additional wffs attached).

3. The above two rules are the only rules of forming wffs.

Using the first method, therefore, finite strings such as

$$v_2,\alpha v_1{v}_2,\text{and}\mathit{\hspace{1em}\hspace{1em}}\beta v_3\alpha v_2\beta v_1{v}_1{v}_3{v}_2$$

are well-formed formulas, while

$$v_2{v}_3,v_1\alpha v_2{v}_1,\text{and}\mathit{\hspace{1em}\hspace{1em}}\beta v_2{v}_3$$

are not, where $\alpha$ and $\beta$ are binary and ternary connectives respectively, and $v_i$ are atoms.

Notice that in the last two methods, auxiliary symbols, such as the parentheses and the comma, are introduced to help the comprehensibility of wffs. Therefore, the third wff above becomes

$$(\beta v_3(\alpha v_2(\beta v_1{v}_1{v}_3))v_2)$$

using the second method, and

$$\beta (v_3,\alpha (v_2,\beta (v_1,v_1,v_3)),v_2)$$

using the third method.

Remark. It is customary is to infix the connective between the two wffs, when the connective is binary, so that $(\alpha pq)$ or $\alpha (p,q)$ becomes $(p\alpha q)$. Parentheses become necessary when using the infix notations, so as to avoid ambiguity. For example, is

$$p\vee q\wedge r$$

constructed from $p\vee q$ and $r$ via $\wedge$, or $p$ and $q\wedge r$ via $\vee$? Both are possible!

Formation of All Well-formed Formulas

Pick a method of forming wffs above, say, the first method. Rules 1 and 2 above suggest that if we were to construct the set $\overline{V}$ of all wffs, we need to start with the set $V$ of atoms. From $V$, we next form the set of wffs of the form $\alpha p_1\mathrm{\cdots }{p}_n$, where each $p_i$ is an atom, and where $\alpha$ ($n$-ary) ranges over the entire set $F$. This will go one indefinitely. In other words, we construct $\overline{V}$ inductively as follows:

1. $V_0:=V$,

2. $V_{i+1}:=V_i\cup {\bigcup }_{\alpha \in F}\{\alpha p_1\mathrm{\cdots }{p}_n\mid \alpha \text{ is }n\text{-ary and each }{p}_j\in V_i\}$,

3. $\overline{V}:={\bigcup }_{i=0}^{\mathrm{\infty }}{V}_i$.

Notice that constants are in every $V_i$ where $i>0$.

It can be shown that every wff can be uniquely written as $\alpha p_1\mathrm{\cdots }{p}_n$ for some $n$-ary connective and wffs $p_i$ in $\overline{V}$. This is called the unique readability of wffs.

Furthermore, $\overline{V}$ has a natural algebraic structure, as we may associate each $\alpha \in F$ a finitary operation $[\alpha ]$ on $\overline{V}$, given by $[\alpha ](p_1,\mathrm{\dots },p_n)=\alpha p_1\mathrm{\cdots }{p}_n$. By defining $[F]:=\{[\alpha ]\mid \alpha \in F\}$, we see that $\overline{V}$ is closed under each operation in $[F]$, or that $\overline{V}$ is an inductive set over $V$ with respect to $[F]$. In fact, it is the smallest inductive set over $V$ (See Rule 3 above).

Finally, if $F$ is finite, it is not hard to see that $\overline{V}$ is effectively enumerable, and there is an algorithm deciding whether a string is a wff or not.

Title	construction of well-formed formulas
Canonical name	ConstructionOfWellformedFormulas
Date of creation	2013-03-22 18:52:20
Last modified on	2013-03-22 18:52:20
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	10
Author	CWoo (3771)
Entry type	Feature
Classification	msc 03B05