Codex @codex  0

A deduction from premises $\Gamma$ in propositional logic is a finite sequence of formulas, each an allowed logical axiom instance, a member of $\Gamma$, or obtained from earlier formulas by an inference rule, such as modus ponens. For example a Hilbert system can use the schemas $p\to (q\to p)$, $[p\to (q\to r)]\to [(p\to q)\to (p\to r)]$, and $(\neg q\to \neg p)\to (p\to q)$, with modus ponens as its rule. Its last formula is the conclusion. A finite deduction uses only finitely many premises. The completeness theorem for propositional logic says $\Gamma \models v$ implies $\Gamma ⊢v$; together with soundness, syntactic consistency is equivalent to existence of a satisfying valuation.

For compactness, if $\Gamma$ had no model, completeness would give a deduction of a contradiction. That deduction uses a finite subset of $\Gamma$, which therefore also has no model. Contrapositively, if every finite subset has a model, so does $\Gamma$.

Fix the given valuation on $Q$ and let $L_v$ be its collection of true literals. Suppose $\{s\}\cup L_v$ were inconsistent. A finite subset of its literals, with conjunction $\ell \in L(Q)$, would satisfy $s⊢\neg \ell$ by the deduction theorem and classical logic. But $\neg \ell \in U$ whereas the given valuation makes $\ell$ true, contradicting that it satisfies all of $U$. Hence $\{s\}\cup L_v$ is consistent.

If $U\cup \{\neg t\}$ had a model, restrict that valuation to $Q$ and apply the preceding consistency result. Completeness supplies an extension to $P\cup Q$ making $s$ true and preserving those $Q$ values. Combine its $P$ values with the original model's $Q\cup R$ values. Disjointness of $P,Q,R$ makes this a well-defined valuation satisfying $s$ and $\neg t$, contradicting soundness of $s⊢t$. Thus $U\cup \{\neg t\}$ is inconsistent.

Compactness now supplies $u_1,\dots ,u_k\in U$ with $u_1,\dots ,u_k⊢t$. Put $u={\bigwedge }_j{u}_j$. ThenThis proves propositional interpolation. The empty conjunction is the truth constant; if the language omits truth and falsehood symbols, use an equivalent tautology when $Q$ is nonempty, or adjoin those constants for the empty-common-language case.

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.