I'm trying to prove a special case of the compactness theorem. Here is a statement of the compactness theorem in this handout.
A set of formulas $\Phi$ is satisfiable iff it is finitely satisfiable.
The special case I'm trying to prove is where the language is fixed as classical propositional calculus and the set of well-formed formulas is constrained to be countable.
I also watched this lecture for background on the compactness theorem, but did not watch the whole section describing the proof. I did watch the part describing the general idea of constructing a $\Delta$ that is equisatisfiable with $\Sigma$, as well as the part describing which cases of the biconditional are trivial. I think the approach taken here is different from the content of the lecture, although I am not certain. I'm trying to prove this result myself as an exercise.
I'm most interested in knowing whether the proof is correct, how to improve it, and if there are alternative approaches that are much simpler.
First a word on notation.
Let $\mathbb{N}$ refer to the positive integers.
Let $\varepsilon$ refer to the empty set.
Let $L$ be the language of classical propositional calculus, consisting of $\land$, $\lor$, $\lnot$, and the set of primitive propositional variables $V$ .
Let $F(w)$ refer to the set of variables that are free in the well-formed formula $w$ .
A model $m$ is a mapping from $V$ to $\{0, 1\}$ .
A partial model $\mu$ is a mapping from a subset of $V$ to $\{0, 1\}$ . A proper partial model is a partial model that is not a model.
Let $M(w)$ refer to the set of partial models on $F(w)$ that are true in $w$ .
For example.
$$ M(A \land \lnot A) = \varepsilon $$
$$ M(A) = \{\{(A, 1)\}\} $$
$$ M(\lnot A \land B) = \{\{(A, 0), (B, 1)\}\} $$
$$ M(\lnot A \lor B) = \{\{(A, 0), (B, 0)\}, \{(A, 0), (B, 1)\}, \{(A, 1), (B, 1)\}\} $$
Let $\Sigma$ be a countably infinite sequence of wffs indexed by the positive integers $\mathbb{N}$. The elements of $\Sigma$ need not be distinct.
Let $\Lambda$ be a directed acyclic graph that is not necessarily a tree defined as follows. The vertices of $\Lambda$, denoted $\Lambda^V$, are ordered pairs of non-negative integers and partial models. For instance, $(0, \{(A, 1), (B, 0)\})$ is an element of $\Lambda^V$ . A directed edge also has a partial model associated to it, in addition to a source and a destination. Self-edges are not permitted. Multiple edges are also not permitted, even if the edges have different content. Let the edges be denoted with $\Lambda^E$ .
Let $\Lambda_0$ be a singleton graph with vertex $(0, \varepsilon)$ .
The vertices of $\Lambda_1$ are taken from the union of $\Lambda^V_0$ and the partial models on $F(\Sigma_1)$ .
Let $\Lambda_1^V$ be $\Lambda_0^V \cup \{(1, \alpha) \mathop. \alpha \in M(\Sigma_1) \}$ . The edges in $\Lambda_1^V$ that aren't in $\Lambda_0$ are the partial models of $\Sigma_1$ together with the index $1$ .
Let $\Lambda_1^E$ be $\{((0, \varepsilon), \alpha ,(1, \alpha))\}$. Each edge in $\Lambda_1$ starts at the unique element of $\Lambda_0^V$ and ends at the vertices that aren't in $\Lambda_0$ . Each edge is labelled by the partial model it corresponds to.
For example, here is the graph $\Lambda_1$ for $\Sigma = \lnot A \lor B, \cdots$ . The edges are directed and pointing down.
(0, ε)
/ | \
{(A,0), (B,1)} / | {(A,0), (B,0)} \ {(A, 1), (B, 1)}
/ | \
(1, {(A,0), (B,1)}) (1, {(A, 0), (B, 0)}) (1, {(A, 1), (B, 1)})
In general, we can define $\Lambda_{n+1}$ in terms of $\Lambda_n$ as follows.
$$ \Lambda^V_{n+1} \stackrel{\text{def}}{=\!=} \Lambda^V_n \cup \{(n+1, \alpha) \mathop. \alpha \in M(\Sigma_1, \cdots, \Sigma_n) \} $$
As a slight abuse of notation let $\Lambda_{n-1}$ be $\varepsilon$ when $n$ is zero.
$$ \Lambda^E_{n+1} \stackrel{\text{def}}{=\!=} \Lambda^E_n \cup \{(\alpha, \beta_2\setminus\alpha_2, \beta) \;\mathop.\; (\alpha \in \Lambda^V_{n} \setminus \Lambda^V_{n-1}) \land (\beta \in \Lambda^V_{n+1} \setminus \Lambda^V_{n}) \land \alpha \subset \beta \} $$
The newest level of each $\Lambda_n$ consists of all the partial models of $\Sigma_1, \cdots, \Sigma_n$ . Each vertex in the second newest level edges going to each of the vertices in the newest level that it's compatible with.
Finally, let $\Lambda$ be defined as follows.
$$ \Lambda^V \stackrel{\text{def}}{=\!=} \bigcup_{i=0}^{\infty} \Lambda_i^V $$
$$ \Lambda^E \stackrel{\text{def}}{=\!=} \bigcup_{i=0}^{\infty} \Lambda_i^E $$
Let the unique element of $\Lambda_0^V$ be called the root of $\Lambda$ .
Lemma 101: $\Lambda$ has an infinite path starting at its root or it does not.
By the law of the excluded middle, (101) is true.
Lemma 102: $\Sigma$ is satisfiable if and only if $\Lambda$ has an infinite path starting at its root
If $\Sigma$ is satisfiable, then there exists a model $m$ that satisfies it.
$m$ also satisfies each $\Sigma_1, \cdots, \Sigma_n$ for all values of $n$ in $\mathbb{N}$ .
Since $m$ is a model, it corresponds to a unique partial model $\mu_n$ associated with every $n$ in $\mathbb{N}$ . More specifically, $\mu_n$ is $m$ restricted to the free variables of $\Sigma_1, \cdots, \Sigma_n$ .
The root of $\Lambda$ has an edge going to $\mu_1$ regardless of what $\mu_1$ is.
If $\Lambda$ has an infinite path starting at its root, let's call it $p$. Let $p_n$ denote the nth edge in $p$ . $p_1$ refers to the edge starting at the root of $\Lambda$ .
The middle element of $p_n$, henceforth denoted $(p_n)_2$ is the content of the edge.
$$j \stackrel{\text{def}}{=\!=} \bigcup_{i=1}^\infty (p_i)_2 \;\;\text{is a partial model}$$
$j$ is satisfiable in $\Sigma$ and assigns $0$ or $1$ to every free variable in $\Sigma$.
Let $U$ be the set of variables in $V$ that are not free variables in $\Sigma$ .
Let $j'$ be defined as $j \cup \{ (\alpha, 1) \mathop. \alpha \in U \}$ . $j'$ is a model that sends all variables that aren't mentioned in $\Sigma$ to true.
$j'$ is a model and $j'$ satisfies $\Sigma$, so $\Sigma$ is satisfiable.
Lemma 103: $\Sigma$ contains a finite contradiction if and only if $\Lambda$ has no infinite path starting at its root
If $\Sigma$ contains a finite contradiction, then it contains a finite subset $\Sigma_0$ with no models. Let $n$ be the greatest index of any element in $\Sigma_0$ .
$\Sigma_1, \cdots, \Sigma_n$ has no models, which means there are no edges coming in to level $n$ of $\Lambda$ . Any infinite path starting at the root in $\Lambda$ must pass through level $n$, therefore there are no infinite paths.
If $\Lambda$ has no infinite path, let $n$ be the length of the longest path in $\Lambda$ . $\Sigma_1, \cdots, \Sigma_{n+1}$ is therefore unsatisfiable, otherwise there would be a path leading to level $n+1$ in $\Lambda$ .
Theorem: A countable set of wff's $\Delta$ is satisfiable if and only if it is finitely satisfiable.
If $\Delta$ is empty, then it is both satisfiable and finitely satisfiable.
If $\Delta$ is finite but not empty, then it is satisfiable if and only if it is finitely satisfiable. After all, $\Delta$ is a finite subset of itself when $\Delta$ is finite.
If $\Delta$ is countably infinite, then it corresponds to a sequence $\Sigma$ and therefore a graph $\Lambda$.
By (101), $\Lambda$ contains an infinite path or it does not.
Suppose $\Lambda$ contains an infinite path, then $\Sigma$ is satisfiable and therefore $\Delta$ is satisfiable.
Suppose $\Lambda$ does not contain an infinite path, then $\Sigma$ contains a finite contradiction and therefore $\Delta$ contains a finite contradiction.
By definition, $\Delta$ does not contain a finite contradiction if and only if it is finitely satisfiable.
Either $\Delta$ is satisfiable or $\Delta$ contains a finite contradiction.
Therefore, $\Delta$ is satsifiable if and only if $\Delta$ is finitely satisfiable.
Best Answer
It seems to me that this is a massively-overcomplicated version of the following argument; the key simplification is in a better choice of $T$, which makes much of the technical detail disappear.
Suppose we have a countable set of propositional variables $V$, and $\Phi$ is a finitely satisfiable set of wffs from $V$. Pick some enumerations of $V$ and $\Phi$ as $\{v_i:i\in\mathbb{N}\}$ and $\{\varphi_i:i\in\mathbb{N}\}$ respectively (it doesn't matter how we do this, we just need some enumeration of each).
Choosing an enumeration of $V$ lets us think of valuations as infinite binary sequences. Choosing an enumeration of $\Phi$, meanwhile, lets us define the following tree $T$ of finite binary sequences:
Basically, a node of length $n$ on $T$ represents a partial truth assignment ("partial model" in your language) for the first $n$ variables of our language which is consistent with the first $n$ formulas of $\Phi$ being true.
We easily show that $T$ must have infinite height since $\Phi$ is finitely satisfiable: to find a node on $T$ of length $n$, just consider the "restriction" of a single valuation making $\bigwedge_{i<n}\varphi_n$ true (which exists by finite satisfiability). Meanwhile, we have that any infinite path through $T$ corresponds to a valuation making every sentence in $\Phi$ true.
We're now done by applying Konig's lemma.
Let me end with a coda which illustrates the value of the above choice of $T$.
If we allow $V$ to be uncountable, then of course everything goes to heck: the analogous "tree" we build will have uncountable height which prevents us from applying the usual Konig's lemma, and it turns out that there isn't really an analogue of Konig's lemma for such trees at all.
However, there is a key property which the binary tree highlights: compactness. The set of paths through the full binary tree is an infinite product of finite (hence compact) spaces, and so is itself compact, and Konig's lemma is just a rephrasing of this compactness.
This suggests that, given an arbitrary set of variables $V$, we look at the set of valuations $2^V$ as a topological space - namely, the "$V$-fold product" of the two-element Hausdorff space. Tychonoff's theorem says that this space is compact, and we can turn this around to get propositional compactness: if $\Phi$ is a set of wffs from $V$, for each $\varphi\in\Phi$ let $U_\varphi\subseteq 2^V$ be the set of valuations not making $\varphi$ true. Since $\Phi$ is finitely satisfiable, no finite subset of $\{U_\varphi:\varphi\in\Phi\}$ covers all of $2^V$; but since $2^V$ is compact per Tychonoff, this means that $\{U_\varphi:\varphi\in\Phi\}$ itself doesn't cover $2^V$ either.
So pick $f\in 2^V$ with $f\not\in\bigcup_{\varphi\in\Phi}U_\varphi$. By definition, $f$ makes each $\varphi\in\Phi$ true. So $\Phi$ is satisfiable!
The point I'm making here is that the simpler combinatorial object makes the underlying topological idea clearer, which in turn suggests a more general topological argument.