construction of wellformed 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 Wellformed Formula
A wellformed formula, or wff for short, is then a special kind of finite string, sometimes called a term, formed in a specific, predetermined 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 wellformed 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 Wellformed 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 wellformed formulas 

Canonical name  ConstructionOfWellformedFormulas 
Date of creation  20130322 18:52:20 
Last modified on  20130322 18:52:20 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  10 
Author  CWoo (3771) 
Entry type  Feature 
Classification  msc 03B05 