Does the language of the propositional calculus belong to some type of languages in Chomsky hierarchy (regular, CFL, CSL, recursive, r.e.)? From https://en.wikipedia.org/wiki/Propositional_calculus#Generic_description_of_a_propositional_calculus

A propositional calculus is a formal system ${\mathcal {L}}={\mathcal {L}}\left(\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I} \right)$. ...


The language of $\mathcal {L}$, also known as its set of formulas, well-formed formulas, is inductively defined by the following rules:


Base: Any element of the alpha set $\mathrm {A}$  is a formula of $\mathcal {L}$.


If $p_{1},p_{2},\ldots ,p_{j}$ are formulas and $f$ is in $\Omega_{j}$, then $\left(f(p_{1},p_{2},\ldots ,p_{j})\right)$ is a formula.


Closed: Nothing else is a formula of $\mathcal {L}$.

Does the language of the propositional calculus $\mathcal {L}$ belong to some type of languages in Chomsky hierarchy (regular, CFL, CSL, recursive, r.e.)?
If yes, why? (what is its grammar?)
Thanks.
 A: When settling for $p, p', p'', \ldots$ as propositoinal variables, sticking to prefix notation and restricting oneself to a fixed set of operators, the language of propositional logic can be given as a context-free grammar:
$\langle \{F, P, U, B\}, \{\neg, \land, \lor, \to, p, ', "(", ")", ","\}, R, F \rangle$, where $R =\{$
$
F \longrightarrow P\\
F \longrightarrow U(F)\\
F \longrightarrow B(F,F)\\
U \longrightarrow \neg\\
B \longrightarrow \land\\
B \longrightarrow \lor\\
B \longrightarrow \to\\
P \longrightarrow p\\
P \longrightarrow P'\\
\}$.
Comments:

*

*selection of operators:
Generalizing over arbitrary $n$-ary connectives is not possible, because the number of symbols on each side of the rule is arbitrary but fixed (so we can not write "$\ldots$"), and there is no such thing as meta-variables either (so we can not write "$f^n$" to indicate that the arity of the operator matches the number of arguments), and the number of terminal nodes and the set of production rules in a formal grammar is finite (so we can not have arbitrary, infinitely many operators).
This is not so much of a problem because normally one does pick a fixed set of operators for one's dialect of propositional logic, and the "If $f$ is an $n$-ary operator ..." clause is only a useful abbreviation for summing up a bunch of cases when writing up the inductive definition, while the actual rule set for that variation the language is finite. It's just that formal grammars can't account for the generalization as the family of all such languages with arbitrary operators.


*propositional variables:
This formulation assumes a simple recursive numbering scheme for propositional variables: $p, p', p'', \ldots$; a numbering scheme in the decimal format as suggested in your source is possible in an analogous manner. Already numbered variables can not be treated as terminal nodes because there are countable infinitely many of them, but as stated above, the definition of a formal grammar requires the set of terminal nodes and the set of production rules to be finite; so one has to settle for some kind of recursive numbering scheme. Again, not much of a problem because there is no reason why you'd want some wild non-recursively enumerable naming scheme for propositoinal variables.


*auxiliary symbols:
Note that in this formulation, the parentheses and the comma are part of the alphabet of the formal language of PL, not of the grammar formalism.


*writing conventions:
Conventions such as infix notation ("$A \land B$" instead of "$\land(A, B)$") and omission of parentheses ("$A \land B \land C$" instead of "$((A \land B) \land C)$", "$A \to B \land C$" instead of "$(A \to (B \land C))$") would have to be appropriately translated into respective production rules as well.


*infix notation:
The rules in infix notation would then be $\{, \ldots, F \longrightarrow UF, F \longrightarrow FBF, \ldots\}$.


*omission of parentheses:
A perhaps interesting point is that operator associativity and precedence would make the language context-sensitive, because the presence or absence of parentheses depends on which context of other operators the subformula occurs in. However, omission of parentheses is usually treated as syntactic sugar on the surface representation while in the underlying formal languages has all parentheses present, so one wouldn't typically explicitly encode these omission rules in the grammar.
