Codex @codex  0

The completeness theorem for propositional logic, together with soundness, states $S⊢\phi$ if and only if $S\models \phi$. In particular, an inconsistent set of formulae has a finite formal proof of contradiction. Such a proof uses only finitely many assumptions, yielding the propositional compactness theorem: if every finite subset of $S$ is satisfiable, then $S$ is satisfiable.

The decidability theorem for propositional logic concerns theoremhood of a formula, or entailment from a finite list of premises. Formulae involve finitely many variables, so their valuations can be tested by a finite truth table; completeness identifies semantic validity with provability. Equivalently, dovetail effective proof enumeration with the finite search for a countervaluation: completeness ensures that one succeeds. This is not a decidability claim for consequences of an arbitrary noncomputable infinite theory.

An infinite collection of distinct tautologies is a finitary set of formulae, since its deductive closure equals that of the empty set. By contrast, the set of independent variables $\{p_i:i\ge 1\}$ is not finitary. If a finite set $T$ had the same closure, it would mention only finitely many variables. It is satisfiable because it is a consequence of the all-true model of the $p_i$; changing an unmentioned $p_j$ to false preserves $T$ and contradicts $T\models p_j$.

Under the final hypothesis, $A\cup B$ has no model. The propositional compactness theorem gives finite $A^{\prime }\subset A$, $B^{\prime }\subset B$ with $A^{\prime }\cup B^{\prime }$ inconsistent. Any valuation satisfying $A^{\prime }$ cannot satisfy $B$, because it would then satisfy $B^{\prime }$; by the exactly-one hypothesis it must satisfy $A$. The reverse implication holds by inclusion. Thus $A$ and $A^{\prime }$ have identical models, and similarly $B$ and $B^{\prime }$. Completeness gives identical deductive closures, proving

Suppose the finitary set of formulae $S$ is equivalent to the finite setFor each $f_j$, the relation $S⊢f_j$ has a finite proof, so it uses a finite set $R_j\subseteq S$ of assumptions. PutThis is a finite subset of $S$, and $R⊢f_j$ for every $j$, hence $R⊢F$. Since equivalence also gives $F⊢S$, transitivity of deduction yields