Te compactness theorem for First Order Logic (FOL) is as follows, from this handout.
A set of sentences $\Sigma$ has a model if and only if every finite subset of $\Sigma$ has a model.
I'm curious whether the compactness theorem can be extended to not-necessarily-closed well-formed formulas. The proof of this fact seems simple enough, but in a few presentations of the compactness theorem that I've seen the stronger statement involving not-necessarily-closed well-formed formulas is not made. Recent experience has also made my wary of free variables.
I'm also curious whether talking about compactness when free variables are involved even makes sense, Wilfrid Hodges' A Shorter Model Theory and David Marker's Model Theory: An Introduction both indirectly exclude open formulas by restricting attention to theories, which are defined as sets of sentences.
My motivation for this question is trying to understand the definition of a type, given below. I'm curious whether it follows from the definition that a given type $t$ is always satisfiable.
Here's my attempt to prove it. The idea is just to reinterpret all the free variables as constant symbols in a different language.
Let $L$ be a language with free variable symbols $V$ and constant symbols $K$. Let $L'$ be a language whose constant symbols are $K \cup V$ and whose variable symbols are $V'$ where $V$ and $V'$ are disjoint.
Let $\Sigma$ be a set of $L$ formulas. $\Sigma$ is satisfiable if and only if there exists a model $M$ and an assignment $v$ such that $M, v \models \Sigma$.
$M, v \models \Sigma$ holds if and only if there exists an $L'$-structure $M'$ such that $M' \models \Sigma$.
Since $\Sigma$ is a set of sentences in $L'$, $M'$ exists by compactness whenever $\Sigma$ is finitely satisfiable.
I'm interested in this result because I want to know if I can conclude that a type $t$ is satisfiable (perhaps in some extended sense of satisfiability).
Here is the definition of a type from Wikipedia, somewhat paraphrased.
Let $M$ be an $L$-structure and $A$ be a subset of the domain of $M$. Let $L(A)$ denote the language in the signature of $L$ extended with constant symbols for each $A$.
An $n$-type of $M$ over $A$ is a collection $t$ of not-necessarily closed well-formed formulas in the language $L(A)$ such that $\mathrm{FV}(t) \subset \{ x_1, x_2, \cdots, x_n \}$. Let $\mathrm{FV}(t)$ denote the union of all $\mathrm{FV}(\varphi)$ for all $\varphi$ in $t$.
For every finite subset $t_0$ in $t$, there exists an $f(t_0)$ in $M^n$ such that $M \models t_0[x_1:=f(t_0)_1,\, x_2:=f(t_0)_2 \cdots]$.
The function $f$ must exist for $t$ to be a type, but it is not itself part of the type. Said another way, it is not possible to create two types that contain the same formulas but have different witness-maps.
Best Answer
There are two forms of the compactness theorem with free variables. The OP correctly states and proves one of these. The second is stated below (CT2). Though CT2 is a simple corollary of the compactness theorem, it is the most natural theorem to apply when dealing with types (it may be what you are looking for).
CT1. If $\Sigma(x)$ is finitely satisfiable, then $\Sigma(x)$ is satisfiable;
CT2. If $\Sigma(x)$ is finitely satisfiable in a model $M$, than $\Sigma(x)$ is satisfiable in an elementary extension of $M$.
It is worthwhile to note that in CT2 we can allow $\Sigma(x)$ to have parameters over $M$.
Finitely satisfiable in $M$ means that $M\models\exists x\ \varphi(x)$ for every $\varphi(x)$ that is conjunction of formulas in $\Sigma(x)$.
The proof of CT2 is an application of CT1 and the diagram method. I sketch the idea below.
Let $a$ be a tuple that enumerates the model $M$. Let $p(z)=\mathrm{tp}_M(a)$, where as usual $\mathrm{tp}(a)=\{\varphi(x):M\models\phi(a)\}$. Verify that $p(z)\cup\Sigma(x)$ is finitely consistent (in $M$). Apply CT1 to obtain a model $N,b,c\models p(z)\cup\Sigma(x)$. Prove that $b$ enumerates an elementary substructure of $N$ isomorphic to $M$. (This last step is what is known as the diagram method.)