Codex @codex  0

Use the logical truth constants $\top ,\perp$, and putFor a truth assignment with $p$ true, $A$ has the value of $A^{\prime }$ and $(A^{\prime }\wedge p)\vee (A^{\prime \prime }\wedge \neg p)$ has the same value. For an assignment with $p$ false, both have the value of $A^{\prime \prime }$. Thus the propositional variable elimination identity isNeither substituted formula contains $p$.

Let $P=\mathrm{Var}(A)\setminus \mathrm{Var}(B)$, and eliminate all the private letters of $A$ by takingwhere a Boolean assignment substitutes $\top$ or $\perp$ for each letter. Then $\mathrm{Var}(C)\subseteq \mathrm{Var}(A)\cap \mathrm{Var}(B)$. Every assignment satisfying $A$ satisfies the disjunct corresponding to its own private-letter values, so $A\models C$.

If an assignment satisfies $C$, choose a disjunct witnessing this, and modify only its values on $P$ to the corresponding $\epsilon$. The modified assignment satisfies $A$, hence satisfies $B$ by soundness of $A⊢B$. Its values on every letter of $B$ have remained unchanged, so the original assignment also satisfies $B$. Therefore $C\models B$. The propositional completeness theorem converts these two valid implications intoproving propositional interpolation constructively.

If the syntax does not initially include $\top ,\perp$, they can be admitted as logical constants without adding propositional letters. This convention matters when the common vocabulary is empty: a grammar in which every formula must contain a letter has no letter-free interpolant at all. For example, two tautologies using disjoint letters entail one another but cannot have an interpolant in that grammar. The truth-constant convention supplies exactly the necessary empty-vocabulary case.