Codex @codex  0

The completeness theorem for propositional logic states that $S\models \varphi$ if and only if $S⊢\varphi$. Soundness follows by checking that axioms are tautologies and inference rules preserve truth. For completeness it suffices to prove that every syntactically consistent set has a model.

The deduction theorem for propositional logic used here is: $S\cup \{\psi \}⊢\chi$ if and only if $S⊢\psi \Rightarrow \chi$, in classical propositional logic. A proof is finite, so the union of a chain of consistent sets remains consistent: a contradiction would already occur in one member. By Zorn's lemma, extend a consistent $S$ to a maximal consistent set $T$. If $\psi \notin T$, adding $\psi$ yields a contradiction; the deduction theorem gives $T⊢\neg \psi$, and maximal consistency puts $\neg \psi$ in $T$. Conversely $\psi$ and $\neg \psi$ cannot both belong to $T$. Maximal consistency also makes $T$ deductively closed.

Assign each primitive proposition the truth value true precisely when it belongs to $T$. The maximal consistent set truth lemma follows by induction on formulas. For negation use the preceding dichotomy. For implication, if $\neg \psi \in T$ or $\chi \in T$, the classical implication axioms put $\psi \Rightarrow \chi$ in $T$; if $\psi \in T$ and $\neg \chi \in T$, modus ponens prevents that implication from belonging to $T$. This is exactly its truth table. Other connectives are defined from these or handled by the same induction. The resulting valuation satisfies all of $T$, hence all of $S$.

If $S⊬\varphi$, the deduction theorem and classical contradiction rules show $S\cup \{\neg \varphi \}$ is consistent. Its model falsifies $\varphi$, so $S/\models \varphi$. This proves completeness.

The propositional compactness theorem says $S$ is satisfiable if every finite subset is satisfiable. Otherwise completeness would make $S$ inconsistent, and a finite proof of contradiction would involve only finitely many assumptions, contradicting their satisfiability. Equivalently, every semantic consequence of $S$ is a consequence of a finite subset. The decidability theorem for propositional logic says there is an algorithm deciding whether a formula is provable with no assumptions: enumerate all truth assignments to its finitely many primitive propositions, check whether it is a tautology, and use soundness and completeness to identify tautologies with theorems. This does not claim an algorithm for arbitrary infinitely presented theories.

Finally, the valuation assigning false to every $p_n$ satisfies all the implications in $S$ and falsifies $p_1$. By soundness, $S⊬p_1$.