I recently came across this way of defining propositional logic:
Let $p \in PV$ be a propositional variable. The set $F$ of propositional formulas is defined by the following grammar:
$$\alpha ::= p | \top | \bot| \lnot \alpha | \alpha \supset \alpha | \alpha \lor \alpha | \alpha \land\alpha$$
I really like this representation because it is so compact and I would like to learn more about it. Can somebody tell me where to find more information about this notation? I guess it is some kind of formal grammar? Any links or textbooks are appreciated :)
To close this question I quote the comment from Andreas