Terms and formulas as finite set codes

For an alphabet token $x$, let $[x]$ denote the one-letter word. If each $u_i$ is either a token or a word, define the fully delimited serialization

where ${\bar{u}}_i=[u_i]$ for a token field and ${\bar{u}}_i=u_i$ for a word field. Concatenation is the set function defined in Set signatures and finite syntax strings, so every displayed constructor below is an actual member of $W_L$.

A leaf term is $\mathrm{enc}(\mathsf{v}\mathsf{a}\mathsf{r},v_i)$ or $\mathrm{enc}(\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t},c)$. A composite term is $\mathrm{enc}(\mathsf{f}\mathsf{u}\mathsf{n},f,t_1,\dots ,t_n)$ with $a(f)=n$. Atomic formulas are $\mathrm{enc}(\mathsf{e}\mathsf{q},s,t)$ and $\mathrm{enc}(\mathsf{r}\mathsf{e}\mathsf{l},R,t_1,\dots ,t_n)$ with $a(R)=n$. Formula constructors are $\mathrm{enc}(\mathsf{n}\mathsf{e}\mathsf{g},\varphi )$, $\mathrm{enc}(\mathsf{a}\mathsf{n}\mathsf{d},\varphi ,\psi )$, and $\mathrm{enc}(\mathsf{e}\mathsf{x}\mathsf{i}\mathsf{s}\mathsf{t}\mathsf{s},v_i,\varphi )$. The punctuation, tag, and symbol fields are tokens; an immediate subexpression field is inserted by concatenating its complete word.

Formally, start with the leaf terms and no formulas, repeatedly apply these serialization maps to the current pair of subsets of $W_L$, and take the two unions over $\omega$. The one-stage map is a function on the set $\mathcal{P}(W_L{)}^2$, so natural recursion applies. Each finite list of arguments appears by a common finite stage; hence the union is closed. Induction on stages puts it inside any constructor-closed pair containing the leaves. These are the least term and formula sets, denoted ${\mathrm{Term}}_L$ and ${\mathrm{Form}}_L$.

We print the familiar abbreviations $f(t_1,\dots ,t_n)$, $s=t$, $R(t_1,\dots ,t_n)$, $\mathrm{\neg }\varphi$, $\varphi \wedge \psi$ and $\mathrm{\exists }{v}_i\varphi$. Define $\varphi \vee \psi :=\mathrm{\neg }(\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )$, $\varphi \to \psi :=\mathrm{\neg }(\varphi \wedge \mathrm{\neg }\psi )$ and $\mathrm{\forall }{v}_i\varphi :=\mathrm{\neg }\mathrm{\exists }{v}_i\mathrm{\neg }\varphi$. In the pure membership signature there is just one binary relation symbol $\in$ and every term is a variable.

Conventions and prerequisites: Set signatures and finite syntax strings, The recursion theorem.