Codex @codex  0

Soundness states that formal derivability implies semantic entailment:For first-order sentences this means that every first-order structure satisfying all assumptions also satisfies every first-order sentence formally derived from them. In the logical formula version one uses the usual restrictions on generalization from assumptions with free variables.

Strong completeness states the converse:Equivalently, every syntactically consistent set of first-order sentences has a first-order model. Equality is interpreted as actual identity, and its usual logical axioms and substitution rules are part of the standard calculus. Both assertions hold for arbitrary sets of assumptions, rather than only finite sets.

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.

Theoremhood is formal derivability with no undischarged assumptions. A logical formula is a theorem of a calculus exactly when it has an assumption-free formal proof.