Satisfaction of a formula

Let $\varphi$ be a $\sigma$-formula of a first-order language $\mathcal{L}[\sigma ]$, and let $\mathcal{I}$ be an interpretation for $\mathcal{L}[\sigma ]$. The interpretation $\mathcal{I}$ satisfies the formula $\varphi$, denoted by $\mathcal{I}\models \varphi$, based on the following inductive rules:

• $\mathcal{I}\models \top$ at all times and never $\mathcal{I}\models \perp$.
• For terms, $t_1$ and $t_2$, $\mathcal{I}\models t_1=t_2⟺t_1$ and $t_2$ are interpreted in $\mathcal{I}$ as the same object in the domain.
• For an $n$-ary predicate $P$ and terms $t_1,...,t_n$, $\mathcal{I}\models P(t_1,...,t_n)⟺P(t_1,...,t_n)$ is true in $\mathcal{I}$.
• For a formula $\varphi$, $\mathcal{I}\models \neg (\varphi )⟺\mathcal{I}\models \varphi$ does not hold.
• For formulas $\varphi$ and $\phi$, $\mathcal{I}\models (\varphi \wedge \phi )⟺\mathcal{I}\models \varphi$ and $\mathcal{I}\models \phi$.
• For formulas $\varphi$ and $\phi$, $\mathcal{I}\models (\varphi \vee \phi )⟺\mathcal{I}\models \varphi$ or $\mathcal{I}\models \phi$.
• For formulas $\varphi$ and $\phi$, $\mathcal{I}\models (\varphi \to \phi )⟺\mathcal{I}\models (\neg \varphi \vee \phi )$.
• For formulas $\varphi$ and $\phi$, $\mathcal{I}\models (\varphi ⟺\phi )⟺\mathcal{I}\models ((\varphi \to \phi )\wedge (\phi \to \varphi ))$.
• For a variable $x$ and a formula $\varphi$, $\mathcal{I}\models (\exists x)(\varphi )⟺$ for all objects $d\in D$, $\mathcal{I}\models \varphi (x/d)$. For a $D$ of finite size, $\mathcal{I}\models (\exists x)(\varphi )$ equals $\models {\bigvee }_{d\in D}(x/d)$.
• For a variable $x$ and a formula $\varphi$, $\mathcal{I}\models (\forall x)(\varphi )⟺$ for all objects $d\in D,\mathcal{I}\models \varphi (x/d)$. For a $D$ of finite size, $\mathcal{I}\models (\forall x)(\varphi )$ equals $\mathcal{I}\models {\bigwedge }_{d\in D}\varphi (x/d)$.

Notation: in the formulas above, $\varphi (x/d)$ denotes the formula obtained from $\varphi$ in which all free occurrences of $x$ are substituted for the object $d$.