Is there a "tree-like" proof of compactness theorem in the case of uncountably many variables?

I like proofs using trees and König's lemma, since they are very visual.

One of the applications of König's lemma you can show to students is proving compactness theorem for propositional calculus, which says that a set of formula is satisfiable if and only if every finite subset is satisfiable.

In this proof you have to order the statements in your theory into a sequence and order the variables accordingly. Then you construct a tree in which each vertex corresponds to truth values of a variables from the statements $T_1,\dots,T_n$ and then infinite branch gives you interpretation of all variables which is consistent with the whole theory.

In this way you can prove the compactness theorem under the assumption that the set of variables is countable.

Is there a proof in the similar spirit which works for arbitrary sets of variables too? (Or some technique which can be used to obtain uncountable version if we already have countable version?)

I am interested mainly in the proofs avoiding the use of completeness theorem.

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$.

Here is a way to prove compactness for propositional logic in terms of trees. As Andreas mentions in the comments, the tree property for $\omega$ is not enough. Instead, we can use a two-cardinal variation of the tree property.

If $\kappa$ is a regular cardinal and $\lambda \ge \kappa$, a $(\kappa,\lambda)$ tree $T$ is a set of $2$-valued functions whose domains are elements of $\mathcal{P}_\kappa(\lambda)$ (that is, subsets of $\lambda$ of size $<\kappa$) such that

• the restriction of every function in $T$ is in $T$, and
• every element of $\mathcal{P}_\kappa(\lambda)$ is the domain of some function in $T$.

A cofinal branch of $T$ is a function $f:\lambda \to 2$ such that $f \restriction s \in T$ for every $s \in \mathcal{P}_\kappa(\lambda)$. There is a principle TP$(\kappa,\lambda)$, isolated by Weiss, that says that every thin $(\kappa,\lambda)$ tree has a branch. We don't need to use the definition of "thin", because it is automatic if $\kappa = \omega$ or more generally if $\kappa$ is a strong limit cardinal.

If $\kappa$ is a strongly inaccessible cardinal, then TP$(\kappa,\lambda)$ holds if and only if $\kappa$ is $\lambda$-compact, so it is a large cardinal property. However, TP$(\omega,\lambda)$ can be proved to hold in ZFC: Take an ultrafilter $U$ on $\mathcal{P}_\omega(\lambda)$ that is fine, meaning that it contains the set $\{s \in \mathcal{P}_\omega(\lambda) : \alpha \in s\}$ for every $\alpha < \lambda$. Because we are not requiring any amount of completeness, such an ultrafilter exists by Zorn's lemma. Given an $(\omega,\lambda)$-tree $T$, choose for each set $s \in \mathcal{P}_\kappa(\lambda)$ some function $f_s \in T$ with domain $s$. Then we can define a branch $f$ of $T$ by $f(\alpha) = 1$ if and only if $f_s(\alpha) = 1$ for $U$-almost every $s \in \mathcal{P}_\omega(\lambda)$.

Now we can use this tree property to find a truth assignment for a set $S$ of propositional formulas. By enlarging $S$ we may assume that it is closed under subformulas and in particular that every propositional variable appearing in a formula in $S$ is itself in $S$. Define an $(\omega, S)$-tree $T$ consisting of all consistent truth assignments defined on finite subsets $s$ of $S$. (Strictly speaking we ought to fix a bijection between $S$ and $|S|$ here.) By consistent I mean, for example, that if the formulas $\varphi$, $\psi$, and $\varphi \wedge \psi$ are all in $s$, then $\varphi \wedge \psi$ is assigned the value 1 if and only if both $\varphi$ and $\psi$ are. Assuming TP$(\omega,|S|)$, this tree has a branch, and such a branch is a truth assignment that satisfies all the formulas in $S$.