= Solution
The <completeness theorem for propositional logic>, together with soundness, states $S\vdash\varphi$ if and only if $S\models\varphi$. 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\ge1\}$ 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'\subset A$, $B'\subset B$ with $A'\cup B'$ inconsistent. Any valuation satisfying $A'$ cannot satisfy $B$, because it would then satisfy $B'$; by the exactly-one hypothesis it must satisfy $A$. The reverse implication holds by inclusion. Thus $A$ and $A'$ have identical models, and similarly $B$ and $B'$. Completeness gives identical deductive closures, proving
$$
\boxed{A\text{ and }B\text{ are finitary}}.
$$
Back to article page
