Suppose that $\mathrm{M}$ is a transitive model of ZFC and that $P$ is a forcing notion of $\mathrm{M}$. If $p\in P$ and $\varphi(\tau_1,...,\tau_n)$ is a first-order formula , where the $\tau_i$ are P-names , we say that $p$ forces $\varphi$ if, for every generic ideal $G\subset P$ containing $p$, the generic extension $\langle\mathrm{M}[G],\in\rangle$ is a model of $\varphi$. The Fundamental Theorem of Forcing states that every formula $\varphi$ that holds in $\mathrm{M}[G]$ is forced by some $p\in P$, but before proving this, there are many intermediate results that we must deduce.
First, we show that a special case of the Fundamental Theorem holds for atomic formulas of the form $x_1\equiv x_2$. If $\sigma_1,\sigma_2$ are P-names, denote by $\text{nr}(\sigma_1,\sigma_2)$ the maximum of their name ranks. Let us recursively define a sequence of sets $\mathcal{F}\alpha$ ranging over all ordinals $\alpha$ in $\mathrm{M}$, so that $\mathcal{F}\alpha$ is the set of ordered triples $(p,\tau_1,\tau_2)\in P\times N_\alpha^2$ satisfying the following conditions:
1. For every $(\sigma_1,q_1)\in\tau_1$ with $q_1\supset p$, there exists $(\sigma_2,q_2)\in\tau_2$ such that $q_2\supset q_1$ and $(q_2,\sigma_1,\sigma_2)\in\mathcal{F}{\text{nr}(\sigma_1,\sigma_2)}$.
2. For every $(\sigma_2,q_2)\in\tau_2$ with $q_2\supset p$, there exists $(\sigma_1,q_1)\in\tau_1$ such that $q_1\supset q_2$ and $(q_1,\sigma_1,\sigma_2)\in\mathcal{F}{\text{nr}(\sigma_1,\sigma_2)}$.
How can we interpret this complicated definition? In short, $\mathcal{F}\alpha$ contains the triple $(p,\tau_1,\tau_2)$ if and only if $p$ forces the equality $\tau_1^G \equiv \tau_2^G$ in $\mathrm{M}[G]$, and $\tau_1,\tau_2$ have name rank $\alpha$. The first condition will enforce that $p$ forces $\tau_2^G$ to contain all of the elements that $\tau_1^G$ contains, and the second condition enforces that $p$ forces $\tau_1^G$ to contain all of the elements that $\tau_2^G$ contains (hence the symmetry between the two statements). This means that $p$ forces $\tau_1^G\equiv \tau_2^G$ for all triples $(p,\tau_1,\tau_2)\in\mathcal{F}\alpha$.
This yields the following result:
Theorem 1. Let $\tau_1$ and $\tau_2$ be P-names of rank at most $\alpha$. Then:
1. A generic ideal $G\subset P$ satisfies $\tau_1^G=\tau_2^G$ iff some element $p\in G$ forces $\tau_1 = \tau_2$.
2. An element $p\in P$ forces $\tau_1=\tau_2$ iff $(p,\tau_1,\tau_2)\in\mathcal{F}_\alpha$.
Now we can define a generalization of the sets $\mathcal{F}_\alpha$ which apply to arbitrary formulas $\varphi$, not just the atomic equality formula. We define it casewise recursively as follows:
If $\varphi$ has the form $x_1\in x_2$, then let $\mathcal{F}^\varphi_\alpha$ be the set of tuples $(p,\tau_1,\tau_2)$ such that the set of $q$ which force $\tau_1=\sigma$ for some $(\sigma,q)\in\tau_2$ is dense above $p$.
If $\varphi$ has the form $\neg\psi(x_1...x_n)$, then let $\mathcal{F}^\varphi_\alpha$ be the set of tuples $(p,\tau_1,...,\tau_n)$ such that no extension of $p$ forces $\psi(\tau_1...\tau_n)$.
If $\varphi$ has the form $(\psi_1\rightarrow\psi_2)(x_1...x_n)$, then let $\mathcal{F}^\varphi_\alpha$ be the set of tuples $(p,\tau_1,...,\tau_n)$ such that every extension of $p$ that forces $\psi_1(\tau_1...\tau_n)$ has an extension that forces $\psi_2(\tau_1...\tau_n)$.
If $\varphi$ has the form $(\forall x)\psi(xx_1...x_n)$, then let $\mathcal{F}^\varphi_\alpha$ be the set of tuples $(p,\tau_1,...,\tau_n)$ such that the set of $q$ forcing $\psi(\tau\tau_1...\tau_n)$ is dense above $p$.
This yields the Fundamental Theorem:
Theorem 2. (Fundamental Theorem of Forcing) Let $\tau_1,...,\tau_n$ be P-names of rank at most $\alpha$. Then
1. For any generic ideal $G\subset P$, we have that $\mathrm{M}[G]$ is a model of $\varphi(\tau_1^G...\tau_n^G)$ if and only if some $p\in G$ forces $\varphi(\tau_1...\tau_n)$.
2. An element $p\in P$ forces $\varphi(\tau_1...\tau_n)$ if and only if $(p,\tau_1,...,\tau_n)\in\mathcal{F}^\varphi_\alpha$.