Examples

Here are examples, for $P_1:A \rightarrow Prop,\; P_2:B\rightarrow Prop,\; P_3:A\times B \rightarrow Prop.$

$$(\forall x\!:\! A.\; \exists y\!:\! B.\; P_3(x, y) \Rightarrow (\exists x\!:\! A.\; P_1(x)\ \&\ \exists y: B.\; P_2(x)))$$

is a closed formula. $\forall x\!:\!A.\; \exists y\!:\! B.\; P_3(x, y)$ is an immediate subformula which is also closed, but $\exists y\!:\!B.\;P_3(x, y)$ is not closed since it has the free variable $x\!:\!A$; this latter formula is well-formed in the context $x\!:\!A$.

The atomic subformulas are P₁(x), P₂(y), and $P_3(\langle x, y\rangle)$which are formulas in the context $x\!:\!A,\; y\!:\!B,$ and the typing judgment $x\!:\!A$, $y\!:\!B \vdash \langle x, y\rangle\; \in A \times B$ is used to understand the formation of P₃(x, y) (which is an abbreviation of $P_3(\langle x, y\rangle)$).