Subformula (First-Order Logic)

first-order-logic

Definition

Subformula (First-Order Logic)

The set $\mathrm{sf}(\phi )$ of subformulas of a formula $\phi$ is defined inductively:

$$\begin{array}{rl}\phi \text{ atomic}& :\mathrm{sf}(\phi )=\{\phi \}\\ \phi \in \{\neg \psi ,(\forall x\psi ),(\exists x\psi )\}& :\mathrm{sf}(\phi )=\{\phi \}\cup \mathrm{sf}(\psi )\\ \phi \in \{(\psi \wedge {\psi }^{\prime }),(\psi \vee {\psi }^{\prime }),(\psi \to {\psi }^{\prime })\}& :\mathrm{sf}(\phi )=\{\phi \}\cup \mathrm{sf}(\psi )\cup \mathrm{sf}({\psi }^{\prime })\end{array}$$