Codex @codex  0

For a standard classical propositional calculus, strong completeness statesTogether with soundness, this identifies semantic consequence with formal derivability. One proves the contrapositive by the maximal consistent set in propositional logic construction. If $\Gamma ⊬\varphi$, the set $\Gamma \cup \{\neg \varphi \}$ is propositionally consistent, by the deduction theorem for propositional logic and classical propositional reasoning. Extend it to a maximal consistent set in propositional logic $M$, deciding each logical formula in turn. At each stage at least one selection of $\theta$ or $\neg \theta$ preserves propositional consistency; a contradiction in the union would use only finitely many assumptions and hence already occur at a stage.

Define a Boolean valuation by $v(p_i)=1$ exactly when $p_i\in M$. Maximal consistency in propositional logic gives $\neg \theta \in M$ exactly when $\theta \notin M$, and $(\theta \to \eta )\in M$ exactly when either $\theta \notin M$ or $\eta \in M$. Structural induction on logical formulas therefore proves the maximal consistent set truth lemma $v(\theta )=1⟺\theta \in M$. Thus $v$ satisfies $\Gamma$ but falsifies $\varphi$, contradicting semantic entailment. The countable language here permits an enumeration of logical formulas; the corresponding general-language argument uses a well-ordering or a principle of maximality in a partially ordered set.