How to formally define this language of nested parentheses?

Question

In a lot of logic textbooks, we are given a set of variables $Prop$, and a set of binary connectives, and we build a formal language, using infix notation, from these and also parentheses (, ). However, these books also use nested layers of parenthesis, as abbreviations. So, for example, $[x+(y+z)]$ is an abbreviation of a well-formed formula. I want to make this abbreviation formal. To simplify, and make precise my question, suppose our alphabet is $\{x, +, (,), [,]\}$. I want to formally define a language, by saying that we use $($ and $)$ as innermost parentheses, then $[$ and $]$ as the next layer, then cycle back to $($ and $)$, cycling back and forth, as the depth of the formula increases. Of course, a generalization of my question is using $n$ pairs of parentheses $(_1, )_1, ..., (_n, )_n$, cycling from $1<2<...<n<1$. I would be very happy if someone answered my generalized question.

Answer 1

For any finite number of "types" of parentheses, you can define a context free grammar to formalize the well-formed formulas. For the case of two types of parentheses for example, you would have the following, where $R$ is the root node:

$$ \begin{align*} R &\to S \ \mid \ T \\ S &\to x \ \mid \ \left ( \ T + T \ \right ) \\ T &\to x \ \mid \ \left [ \ S + S \ \right ] \\ \end{align*} $$

In the general case of $n$ types of parentheses $()_0, \ldots, ()_{n-1}$, you would have the following rules for each $i = 0, \ldots, n-1$.

$$ \begin{align*} R &\to S_0 \ \mid \cdots \ \mid \ S_{n-1} \\ S_i &\to x \ \mid \ \left (_i \ S_{(i+1) \ \text{mod} \ n} + S_{(i+1) \ \text{mod} \ n} \ \right )_i \\ \end{align*} $$

This allows for the expressions to start with any arbitrary symbol, but cycles correctly. I think you can't write a context-free grammar if you always want to start with $()_0$ at the lowest level because it involves predetermining a fixed depth for a formula in some form, but I'm not so sure about this.