[proofplan] The argument is a three-line transfer of finiteness from the syntactic side of the calculus to the semantic side. By the [Completeness Theorem](/theorems/1457), the semantic consequence $S \models t$ implies the existence of a formal proof $S \vdash t$. Any formal proof is, by definition, a finite sequence of formulas, so it uses only finitely many hypotheses from $S$ — call this finite set $S'$. Then $S' \vdash t$ by the same proof, and by the [Soundness Theorem](/theorems/1453) we recover $S' \models t$. The theorem is therefore an indirect witness to the fact that the propositional calculus proof system is **finitary**: semantic truth, though defined over possibly infinite sets of valuations, is always certified by a finite piece of syntax. [/proofplan] [step:Convert the semantic hypothesis into a formal proof via Completeness] By hypothesis $S \models t$, i.e.\ every valuation $v: L \to \{0, 1\}$ with $v(s) = 1$ for all $s \in S$ also satisfies $v(t) = 1$. The [Completeness Theorem](/theorems/1457) for propositional calculus asserts that for any $S \subseteq L$ and $t \in L$, \begin{align*} S \models t \iff S \vdash t. \end{align*} The forward direction applies here: there exists a formal proof of $t$ from $S$, that is, a finite sequence of formulas \begin{align*} \varphi_1, \varphi_2, \dots, \varphi_N \end{align*} such that $\varphi_N = t$ and each $\varphi_i$ is either (i) an axiom of the calculus, (ii) an element of $S$, or (iii) obtained from two earlier formulas $\varphi_j, \varphi_k$ with $j, k < i$ by an inference rule (Modus Ponens). [guided] We are handed a *semantic* hypothesis — truth under every model — and we want to conclude a *finite* statement. The tool that bridges semantics and syntax is the [Completeness Theorem](/theorems/1457), which states \begin{align*} S \models t \iff S \vdash t \end{align*} for all $S \subseteq L$, $t \in L$. The forward direction ("every consequence is provable") is exactly what we need: it lets us replace "for every valuation..." by "there exists a formal proof". Why is this move crucial? Because formal proofs are **finite by definition**, whereas a priori the set of valuations satisfying $S$ could be uncountable and a semantic argument could involve infinitely many cases. Applying Completeness to the hypothesis $S \models t$, we extract a proof: a finite sequence \begin{align*} \varphi_1, \varphi_2, \dots, \varphi_N \end{align*} with $\varphi_N = t$ and each line $\varphi_i$ falling into one of three categories — an axiom, a member of $S$, or a Modus Ponens consequence of two earlier lines. The length $N$ is a fixed natural number; this is the whole content of finiteness. [/guided] [/step] [step:Extract the finite set of hypotheses actually used in the proof] Define \begin{align*} S' &:= \{\varphi_i : 1 \le i \le N,\ \varphi_i \in S\}. \end{align*} That is, $S'$ is the set of lines of the proof that are hypotheses from $S$ (as opposed to axioms or Modus Ponens conclusions). Since $\{\varphi_1, \dots, \varphi_N\}$ has at most $N$ elements, $S' \subseteq S$ is finite, with $|S'| \le N$. We claim $S' \vdash t$. Indeed, the identical sequence $\varphi_1, \dots, \varphi_N$ witnesses a formal proof from $S'$: every line is still either an axiom, a member of $S'$ (by construction of $S'$), or a Modus Ponens consequence of two earlier lines. No line requires a hypothesis outside $S'$, because every hypothesis-line of the original proof was placed in $S'$. [guided] Formal proofs are a finite object, and a finite object can only reference finitely many external hypotheses. Which ones? Exactly those that appear as lines of the proof. We therefore *define* \begin{align*} S' &:= \{\varphi_i : 1 \le i \le N,\ \varphi_i \in S\}. \end{align*} Let us check what this gives us: **$S'$ is finite.** The proof has exactly $N$ lines, so the set of lines that happen to be members of $S$ has cardinality at most $N$, hence finite. **$S' \subseteq S$.** Immediate from the definition. **$S' \vdash t$.** We must produce a formal proof of $t$ from $S'$. The natural candidate is the original proof sequence $\varphi_1, \dots, \varphi_N$. Let us verify it is still a legitimate proof when the hypothesis set is restricted to $S'$. For each line $\varphi_i$: - if $\varphi_i$ was an axiom in the original proof, it remains an axiom now; - if $\varphi_i$ was obtained by Modus Ponens from $\varphi_j, \varphi_k$ with $j, k < i$, that inference is unchanged — the rule does not care about the hypothesis set; - if $\varphi_i$ was an element of $S$ (a hypothesis-line), then by construction of $S'$ we have $\varphi_i \in S'$, so $\varphi_i$ is a hypothesis-line relative to $S'$ as well. In every case, the justification of $\varphi_i$ as a proof line is unchanged. The final line is still $\varphi_N = t$. Hence $S' \vdash t$. Why does this step work? Because the proof "forgets" elements of $S$ that never appeared — only the hypotheses actually cited matter. This is the finitary character of syntactic deduction. [/guided] [/step] [step:Return from syntax to semantics via Soundness] We now apply the [Soundness Theorem](/theorems/1453) for propositional calculus, which states that for any $T \subseteq L$ and $\psi \in L$, \begin{align*} T \vdash \psi \implies T \models \psi. \end{align*} Applying this to $T = S'$ and $\psi = t$, and using $S' \vdash t$ from the previous step, we obtain $S' \models t$. Since $S' \subseteq S$ is finite, this establishes the theorem. [guided] We have shown $S' \vdash t$ with $S' \subseteq S$ finite. The theorem asks for $S' \models t$, so we need to return to the semantic side. The [Soundness Theorem](/theorems/1453) provides exactly this direction: \begin{align*} T \vdash \psi \implies T \models \psi \end{align*} for any set of formulas $T$ and any formula $\psi$. This is the "easier half" of completeness — it says that the proof system does not prove falsehoods, which is verified by inducting on proof length and checking that each axiom is a tautology and each inference rule preserves truth under every valuation. Applying Soundness with $T = S'$ and $\psi = t$: since $S' \vdash t$, we conclude $S' \models t$. Combining with $S' \subseteq S$ finite from the previous step, we have found a finite subset $S'$ of $S$ with $S' \models t$, which is precisely the statement of the theorem. One might wonder why we needed the round trip $\models \to \vdash \to \models$ rather than a direct semantic argument. The reason is that "finite" is a syntactic notion — proofs, being combinatorial objects, are finite by definition, whereas semantic consequence is a statement about a potentially infinite class of valuations. Completeness and Soundness together constitute the dictionary that lets us transport finiteness through. [/guided] [/step]