How to put this recursive definiton:
Definition. (Gentzen) subformulas of A are defined by
(a) A is a subformula of A;
(b) if B ◦ C is a subformula of A then so are B, C, for ◦ = →,∧,∨;
(c) if ∀xB or ∃xB is a subformula of A, then so is B[x := t], for all t free for x in B.
in a formal way (without recursion)?
The collection of subformulas of $A$ is the intersection of all the sets $\mathcal X$ that have the following properties:
(1) $A\in\mathcal X$.
(2) If $B\circ C\in\mathcal X$ with $\circ\in\{\to,\land,\lor\}$ then also $B\in\mathcal X$ and $C\in\mathcal X$.
(3) If $\forall x\,B\in\mathcal X$ or $\exists x\,B\in\mathcal X$ then also $B[x:=t]\in\mathcal X$ for all $t$ free for $x$ in $B$.
