The argument is basically correct, but it could stand to be fleshed out a bit. For convenience I’ll write $\mathbf{T}$ and $\mathbf{F}$ instead of $\text{TRUE}$ and $\text{FALSE}$. I’ll also write $m(p_k)=\mathbf{T}$ to indicate that $p_k$ is true in the model $m$.
Let $S_n$ be the set of all formulas in $S$ containing at most the propositional variables $p_1,\dots,p_n$. There is a finite set $E_n\subseteq S_n$ such that every formula in $S_n$ is equivalent to one in $E_n$, so $S_n$ has a model $m_n$. Note that for any $n\in\Bbb Z^+$, each model $m_k$ with $k\ge n$ assigns $p_n$ a truth value.
Let $N_1=\Bbb Z^+$. Each $m_n$ with $n\in N_1$ assigns $p_1$ a truth value. Let $T_1=\{n\in N_1:m_n(p_1)=\mathbf{T}\}$. If $T_1$ is infinite, set $m(p_1)=\mathbf{T}$, and let $N_2=\{k\in T_1:k\ge 2\}$. Otherwise, set $m(p_1)=\mathbf{F}$, and let $N_2=\{k\in N_1\setminus T_1:k\ge 2\}$. Note that in both cases $N_2$ is infinite, $m_k(p_1)=m(p_1)$ for all $k\in N_2$, and $m_k(p_2)$ is defined for each $k\in N_2$.
Now repeat the process. Let $T_2=\{n\in N_2:m_n(p_2)=\mathbf{T}\}$. If $T_2$ is infinite, set $m(p_2)=\mathbf{T}$, and let $N_3=\{k\in T_2:k\ge 3\}$. Otherwise, set $m(p_2)=\mathbf{F}$, and let $N_3=\{k\in N_2\setminus T_2:k\ge 3\}$. In both cases $N_3$ is infinite, $m_k(p_2)=m(p_2)$ for each $k\in N_3$, and $m_k(p_3)$ is defined for each $k\in N_3$.
For the general step, given an infinite $N_n\subseteq\Bbb Z^+$ such that $m_k(p_n)$ is defined for each $k\in N_n$, let $T_n=\{k\in N_n:m_k(p_n)=\mathbf{T}\}$. If $T_n$ is infinite, set $m(p_n)=\mathbf{T}$, and let $$N_{n+1}=\{k\in T_n:k\ge n+1\}\;.$$ Otherwise, set $m(p_n)=\mathbf{F}$, and let $$N_{n+1}=\{k\in N_n\setminus T_n:k\ge n+1\}\;.$$ As before, in both cases $N_{n+1}$ is by construction infinite, $m_k(p_n)=m(p_n)$ for each $k\in N_{n+1}$, and $m_k(p_{n+1})$ is defined for each $k\in N_{n+1}$, so the recursive construction can proceed.
This construction defines a model $m$ that assigns a truth value to each $p_k$. Take any formula $\varphi$ in $S$; it belongs to some $S_n$. Pick any $k\in N_{n+1}$; then $m_k$ is a model for $S_n$ and hence for $\varphi$. Moreover, the construction ensures that $m_k(p_i)=m(p_i)$ for $i=1,\dots,n$, so $m$ is also a model for $S_n$ and hence for $\varphi$.
Specifically - the definition of satisfiability is very similar in modal logic.
This similarity is superficial: there's a crucial way in which modal logic is closer to first-order logic in this respect. In propositional logic a model is basically the same thing as a complete theory: if $\Gamma$ is a maximal complete propositional theory, we just consider the valuation sending a propositional atom $a$ to $\top$ if $a\in\Gamma$ and $\perp$ if $\neg a\in\Gamma$, and check that this is in fact a "model" of $\Gamma$ in the sense of propositional logic.
By contrast, in modal and first-order logic it takes work to go from a complete theory to a model of that theory. Intuitively I'd say that the main point is that semantics in the sense of modal and first-order logic involves things which are not necessarily directly referred to in the language. In modal logic, these are the worlds. A model in the context of modal logic is a family of simple objects (= propositional models) connected to each other in a structured way (the underlying frame). The presence of this additional structure, which isn't explicitly determined by the language, makes the passage from complete theories to models nontrivial and resemble the first-order rather than propositional case.
Best Answer
I don't know a way to make the proof of propositional compactness, for uncountable sets of formulas, look like a tree argument. But if you go back to how König's Lemma is usually proved and apply that argument to the particular tree that you described, then the resulting argument for propositional compactness generalizes quite directly, to the following argument.
Given a set $S$ of propositional formulas, well-order the set of propositional variables occurring in these formulas, and proceed by (transfinite) induction over this well-ordering. When your inductive process arrives at a variable $p$, you assign a truth value to $p$, so as to preserve the following inductive hypothesis:
(*)
For any finite subset $F$ of $S$, there exists a truth assignment that makes $F$ true and agrees with all the values assigned so far in your inductive process.The hypothesis of the compactness theorem is that
(*)
holds at the beginning of your process, before you've assigned values to any of the variables. If (*) holds when you're about to assign a value to $p$, then you can choose that value so as to maintain(*)
. The reason is that if the value "true" for $p$ fails to work because of a finite $F_1\subseteq S$ and "false" fails because of $F_2$, then(*)
already failed before you gave $p$ any truth value, because of $F_1\cup F_2$. You also have to check that(*)
continues to hold at limit stages, but that is easy because any failure at a limit stage, involving a finite $F$ and thus only finitely many variables, would have already been a failure at an earlier stage.After your transfinite induction is complete,
(*)
says that the specific truth values you've assigned to the variables satisfy all finite subsets of $S$ and therefore satisfy $S$.