In Kunen's book Foundation of Mathematics the definition of a well formed expression (wfe) of a lexicon for Polish notation $\langle W, \alpha \rangle$ ($W$ is a set and $\alpha:W\to\omega$ is a function) is given by
- If $s\in W_n$ and $\tau_0,\dots\tau_{n-1}$ are wfe then $s\tau_0\dots\tau_{n-1}$ is a wfe;
where $W_n$ is the collection of all $n$-ary elements of this lexicon for Polish notation , i.e. $W_n = \alpha^{-1}[\{n\}]$.
He latter mention that this definition is given by recursion, using a function $F:\omega\to\wp(W^{<\omega})$, where $F(n)$ is the set of all wfe of length $n$; I tried to write down the function, but I did not succeeded since it seems that one should have the set of all wfe of $\langle W, \alpha \rangle$ before defining the wfe of $\langle W, \alpha \rangle$. I would appreciate any hint.
The definition of :
must start for $n = 0$ with all the finite strings starting with a symbol of arity $0$.
Buy symbols of arity $0$ are symbols without "argument-places" to be filled. Thus the corresponding expressions will be strings of $lenght = 1$ formed by the symbol itself.
I.e. they are the expressions "made of" variables : $x, y, \ldots$ and (if any) individual constants : $c_1, c_2, \ldots$.
The examples in Kunen's book regards terms of first-order arithmetic. If so, we have only one constant : $0$.
Then we "move on" with symbols of arity $1$. This is possible in the language of arithmetic with the (unary) function symbol for the successor function : $S$. In this case we get, e.g. : $Sx, Sy, S0, \ldots$.
Then we have arity $2$, like the (binary) function symbols for sum : $+$ and product : $\times$, generating the terms : $x+y, x \times y, x +0, x +S0, \ldots$.
And so on ...
The easiest case is propositional logic.
You can see Herbert Enderton, A Mathematical Introduction to Logic (2ed - 2001).
We have the set $\mathcal W_0 = \{p_0, p_1, \ldots \}$ of sentential letters.
We hev the propositional connectives : the symbol of arity $1$ : $\lnot$ for negation and the symbols of arity $2$ : $\lor, \land, \rightarrow, \leftrightarrow$.
In this language only $\mathcal W_0, \mathcal W_1$ and $\mathcal W_2$ are not-empty (of course, they are disjoint).
See page 17 for the :
and page 32 for the corresponding ones for Polish Notation :
See [page 30] the description of the Parsing Algorithm :
Finally, see all Section 1.4 : Induction and Recursion [page 34-on] for the Recursion Theorem, which is used to prove the :
Added
The proof is based on the definition by recursion technique :
For any set $A$, any $a_0 \in A$ and any function $G : \omega \times A \to A$, there exists a unique function $\mathcal F : \omega \to A$ such that :
We apply it to the definition of the sequence : $n \mapsto \mathsf {Sent_n}$, where :
In this definition, the set $A$ is the set $℘(\mathcal W^{<ω})$ of all sets of expressions (of the language), $a_0$ is $\mathcal W_0 \in ℘(\mathcal W^{<ω})$ and $G$ is the function which describes $\mathsf {Sent_{n+1}}$ in terms of $\mathsf {Sent_n}$.