Codex @codex  0

Expand the language by constants for $A$ and write $T_A=\mathrm{Th}(\mathcal{M},a{)}_{a\in A}$. An A-type over a structure is a set of formulas in a fixed finite tuple $\bar{x}$, with parameters from $A$, consistent with this complete theory.

Let $Q=\{{\phi }_1(\bar{x}),\dots ,{\phi }_m(\bar{x})\}\subseteq P$. If no tuple of $M$ realized $Q$, thenThat sentence belongs to $T_A$ and contradicts the consistency of $T_A\cup P$. ConsequentlyFor $Q=\varnothing$, any tuple works because domains are nonempty. This proves finite satisfiability; realization of the entire partial type may require an elementary extension.