 An atomic preformula is an expression that results from a sentence of \(\mathcal{L}\) when zero or more terms are replaced by a substitutional variable. A form is an atomic preformula, where the replacement of its substitutional variables with terms yields back a sentence. We can now define a formula of \(\mathcal{L}^{\Sigma}\) recursively. \(A\) is a formula of \(\mathcal{L}^{\Sigma}\) if and only if either (i) \(A\) is a form of \(\mathcal{L}^{\Sigma}\) or (ii) \(A\) is \(\lnot B\), where \(B\) is a formula of \(\mathcal{L}^{\Sigma}\) or (iii) \(A\) is \((B \rightarrow C)\), where \(B\) and \(C\) are each formulas of \(\mathcal{L}^{\Sigma}\) or (iv) \(A\) is \(\Sigma \alpha \ B\), where \(B\) is a formula of \(\mathcal{L}^{\Sigma}\). A sentence of \(\mathcal{L}^{\Sigma}\) is a formula without free substitutional variables.