Past exam of the mathematics course of the University of Cambridge / 2010 / iii / Paper 20 / 4

Fix an effective syntax encoding for the language. Let $E_s$ be the finite set of axioms observed in the first $s$ steps of an enumeration of the given semidecidable axiomatization. These finite approximations can be computed in bounded time, even if the original axiom set is empty or finite. For each $\varphi \in E_s$, form the precisely bracketed logical conjunctionwith $C_0(\varphi )=\varphi$. Let $D=\{C_s(\varphi ):\varphi \in E_s,s\ge 0\}$.

Each $C_s(\varphi )$ is logically equivalent to $\varphi$, so all members of $D$ follow from the original axioms. Every original axiom eventually belongs to some $E_s$, and its corresponding member $C_s(\varphi )$ implies it. Hence $D$ axiomatizes exactly the same theory.

To decide whether a candidate sentence $\psi$ belongs to $D$, let $N$ be its syntactic length. A conjunction of $s+1$ copies has length at least $s+1$, so a representation $\psi =C_s(\varphi )$ can only use $s<N$. Compute each $E_s$ for $s<N$, construct its finitely many candidates, and compare them literally with $\psi$. This finite procedure always terminates and accepts exactly $D$. It does not wait for a nonexistent next axiom, nor assume that conjunction parsing determines the original repeated formula uniquely. Thus $D$ is a decidable equivalent axiomatization, proving the Craig trick.

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.