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.

The propositional completeness theorem states that $\Gamma \models \varphi$ if and only if $\Gamma ⊢\varphi$. Soundness follows by checking the axioms against truth valuations and noting that modus ponens rule preserves truth. For completeness, use the deduction theorem for propositional logic: if $\Gamma \cup \{p\}⊢q$, then $\Gamma ⊢p\Rightarrow q$. In the usual negation rules this also says that a contradiction from $\Gamma \cup \{p\}$ proves $\Gamma ⊢\neg p$.

First construct a maximal consistent set extending any consistent set $\Delta$. Enumerate all formulas, possible because the primitive propositions are countable. Starting with ${\Delta }_0=\Delta$, add formula ${\psi }_n$ at step $n$ if consistency is preserved; otherwise add $\neg {\psi }_n$. This latter addition is consistent: if both extensions gave contradictions, the deduction theorem for propositional logic would prove both $\neg {\psi }_n$ and $\neg \neg {\psi }_n$ from ${\Delta }_n$, a contradiction already in ${\Delta }_n$. The union $M$ is consistent because a finite proof uses only finitely many newly added premises. It decides every formula: exactly one of $\psi ,\neg \psi$ belongs to $M$. It is deductively closed, since an omitted derivable formula would have its negation in $M$, contradicting consistency.

Assign a valuation $v(p)=1$ exactly when the primitive proposition $p$ lies in $M$. Structural induction proves the maximal consistent set truth lemma $v(\psi )=1$ if and only if $\psi \in M$. Negation follows from the decision property. For implication, if $\psi \Rightarrow \chi \in M$ and $\psi \in M$, modus ponens rule gives $\chi \in M$. Conversely, if $\chi \in M$, the elementary implication axioms give $\psi \Rightarrow \chi \in M$. If $\psi \notin M$, then $\neg \psi \in M$, and the usual contradiction rule proves $\psi \Rightarrow \chi$. These two alternatives match the truth table. The other connectives, if primitive, are handled by their corresponding rules or defined from negation and implication. Thus every consistent set has a valuation satisfying it.

Now suppose $\Gamma /⊢\varphi$. If $\Gamma \cup \{\neg \varphi \}$ were inconsistent, the deduction theorem for propositional logic would give $\Gamma ⊢\neg \neg \varphi$. Here the third axiom $\neg \neg \varphi \Rightarrow \varphi$ is essential: it would give $\Gamma ⊢\varphi$, a contradiction. Hence that extension is consistent and has a satisfying valuation. This valuation satisfies $\Gamma$ and falsifies $\varphi$, proving the contrapositive of completeness. In this organization of the proof, the explicit classical double-negation elimination occurs in this last consistency step; the construction and truth lemma use the ordinary negation and contradiction rules, not an unmentioned identification of $\neg \neg \varphi$ with $\varphi$.

The propositional compactness theorem says that a set of formulas is satisfiable exactly when each finite subset is satisfiable. If it were not satisfiable, completeness would make it inconsistent. Its finite contradiction proof uses only a finite subset of premises; soundness makes that subset unsatisfiable. This contradicts the assumed finite satisfiability and proves compactness.

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