Well Formed Expression (Polish Notation) 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.
 A: The definition of :

$F : ω → ℘(\mathcal W^{<ω})$

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 :

formula-building operations (on expressions) defined by the equations
$\mathcal E_¬(\alpha) = (¬ \alpha)$
$\mathcal E_∨(α,β) = (α \lor β)$,
[...];

and page 32 for the corresponding ones for Polish Notation :

$\mathcal D_¬(α) = ¬α, \quad \mathcal D_∨(α,β) = ∨αβ$, [...].

See [page 30] the description of the Parsing Algorithm :

a procedure that, given an expression, both will determine whether or not the expression is a legal wff, and if it is, will construct the tree showing how it was built up from sentence symbols by application of the formula-building operations. Moreover, we will see that this tree is uniquely determined by the wff.

Finally, see all Section 1.4 : Induction and Recursion [page 34-on] for the Recursion Theorem, which is used to prove the :

UNIQUE READABILITY THEOREM : The five formula-building operations, when restricted to the set of wffs,
(a) Have ranges that are disjoint from each other and from the set of sentence symbols, and
(b) Are one-to-one.
In other words, the set of wffs is freely generated from the set of sentence symbols by the five operations.


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 :

$\mathcal F(0) = a_0$ and for all $n < \omega, \mathcal F(n + 1) = G(F(n), n)$.

We apply it to the definition of the sequence : $n \mapsto \mathsf {Sent_n}$, where :

(i) $\mathsf {Sent_0} = \mathcal W_0$ := the set of sentential letters;
(ii) for each $n < \omega, \mathsf {Sent_{n+1}} := \mathsf {Sent_n} \cup \{ \mathcal D_¬(\varphi) : \varphi \in \mathsf {Sent_n} \} \cup \{ \mathcal D_∨(\varphi, \psi) : \varphi, \psi \in {Sent_n} \}$.

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}$.
A: To add a bit to 
Mauro ALLEGRANZA 's post about polish notation
let $ W_1 =  \{N, L, M\} $ and  $ W_2 = \{A, C, E, K \} $
and propostional variables are the lower caseletters
Then p, Np, Cpq, Kpq, Epq, Apq are all wellformed formulas in polish notation.
Also you can replace any propositional variable you with an other propositional variable or with another well formed formula to get another wellformed formula.
Thats all :)
In practice you can check if a formula is wellformed b:


*

*start with a count of 1


Then going left to right in the formula:


*

*for an element of $ W_1$ do nothing

*for an element of $ W_2$ add one

*for a propositional variable substract one

*if you get a count of zero at some point before the end of the formula, then it is not wellformed. (it is to long)

*if you don't get  a count of zero at the end of the formula, then it is not wellformed. (it is to short) 
At the end and only at the end the count should be zero.
Good luck
It is a bit getting used to but polish notation has advantages:


*

*the notation is (much) shorter. 

*no problems with brackets, (there aren't any) 

*easy to see what the main connective is (It is the first connective of the formula)

*very good for term rewriting (condenced detachment)) 

