Propositional calculus logic question

Question

In my assignment I have the following question:

For every proposition $\theta$ let $E(\theta)$ be the set of basic propositions. Prove the following:

For every two propositions, $\alpha$ and $\beta$ such that $\alpha$ is not a contradiction and $\beta$ is not a tautology, if $\alpha \Rightarrow\beta$ then a proposition $\gamma$ exists such that: $\alpha \Rightarrow\gamma$ and $\gamma \Rightarrow \beta$ such that $$E(\gamma)\subseteq E(\alpha) \cap E(\beta)$$

I know the answer is related to DNF, but I can't quite understand the reason behind it.

Answer 1

Form the original paper of William Craig :

• Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory, The Journal of Symbolic Logic, Vol. 22, No. 3 (Sep.1957), pp. 269-285 :

The context of Craig's paper is a generalization of E.W.Beth's work on the first-order notion of definability.

[Beth's result] may be interpreted as showing that [...] the expressive power of each first-order system is rounded out, or the system is functionally complete, in the following sense : any functional relationship which obtains between concepts that are expressible in the system is itself expressible and provable in the system.

Craig states the lemma as :

a useful tool for [investigating] how is a certain modeltheoretic property of a system reflected by theorems in the system.

---

See Raymond Smullyan, First-Order Logic (1968), Ch.XV : Craig's Interpolation Lemma and Beth's Definability Theorem, page 127-on :

A formula $Z$ is called an interpolation formula for a formula $X \rightarrow Y$ if all predicates and parameters of $Z$ occur both in $X$ and in $Y$, and if $X \rightarrow Z, Z \rightarrow Y$ are both valid. Craig's celebrated Interpolation lemma says that for any valid sentence $X \rightarrow Y$ : (i) if $X, Y$ have at least one predicate in common, then there exists an interpolation sentence for $X \rightarrow Y$; (ii) if $X, Y$ have no predicates in common, then either $Y$ is valid or $X$ is unsatisfiable.

We will now adjoin the propositional constants $\top, \bot$ to our language , and so case (ii) can be subsumed under case (i) as follows. If $Y$ is valid, then $X \rightarrow \top$, $\top \rightarrow Y$ are both valid, so then $\top$ is an interpolation formula for $X \rightarrow Y$. If $X$ is unsatisfiable, then $X \rightarrow \bot$, $\bot \rightarrow Y$ are both valid, so then $\bot$ is an interpolation formula for $X \rightarrow Y$.

There is a corresponding interpolation lemma for propositional logic: If $X \rightarrow Y$ is a tautologous formula of propositional logic, then there exists a formula $Z$ (again called an interpolation formula for $X \rightarrow Y$) of propositional logic such that all propositional variables of $Z$ occur in $X$ and in $Y$ and such that $X \rightarrow Z$, $Z \rightarrow Y$ are both tautologies. [For example, $q$ is an interpolation formula for $(p \land q) \rightarrow (p \lor q)$.]

[...]

One important use of Craig's Interpolation Lemma is that it yields a remarkably elegant proof of Beth's Definability Theorem which we now discuss.

Let $P, P_1, \ldots, P_n$ be the predicates which occur in [a first-order theory] $A$, and let us presently assume that P is of [arity] one. $P$ is said to be explicitly definable from $P_1, \ldots, P_n$ in the theory $A$ if there exists a formula $\varphi(x)$ with just one free variable $x$, whose predicates are all in the set $P_1, \ldots, P_n$ (so $P$ is not a predicate of $\varphi(x)$) and such that

$$A \vdash (\forall x) [P(x) \leftrightarrow \varphi(x)],$$

and such a formula $\varphi(x)$ is said to constitute an explicit definition of $P$ from $P_1, \ldots, P_n$ in the theory $A$.

Now we say that the axioms of $A$ implicitly define $P$ from $P_1, \ldots, P_n$ or that $P$ is implicitly definable from $P_1, \ldots, P_n$ in the theory $A$ if the following condition holds: Take a [unary] predicate $P'$ which does not occur in $A$, and let $A'$ be the result of substituting $P'$ for $P$ in every element of $A$. Then $P$ is called implicitly definable from $P_1, \ldots, P_n$ in $A$ if

$$A \cup A' \vdash (\forall x) [P(x) \leftrightarrow P'(x)].$$

Using the completeness theorem, this condition is equivalent to the condition that any two interpretations of $P_1, \ldots, P_n, P$ which satisfy $A$ and which agree on $P_1, \ldots, P_n$ must also agree on $P$ - or stated otherwise, given any values of $P_1, \ldots, P_n$ there is at most one value of $P$ which satisfies the axioms of $A$.

It is obvious that if $A$ defines $P$ explicitly from $P_1, \ldots, P_n$ then it defines $P$ implicitly from $P_1, \ldots, P_n$. For suppose $P$ is explicitly definable from $P_1, \ldots, P_n$ in $A$. Then we have $A \vdash (\forall x) [P(x) \leftrightarrow \varphi(x)]$. Then of course, we also have (for any new predicate $P'$) $A' \vdash (\forall x) [P'(x) \leftrightarrow \varphi(x)]$. Hence $A \cup A' \vdash (\forall x) [P'(x) \leftrightarrow \varphi(x)] \land (\forall x) [P'(x) \leftrightarrow \varphi(x)]$, hence $A \cup A' \vdash (\forall x) [P(x) \leftrightarrow P'(x)]$.

Beth's definability theorem says the converse - i.e. if $A$ implicitly defines $P$ from $P_1, \ldots, P_n$, then $A$ explicitly defines $P$ from $P_1, \ldots, P_n$.

We shall prove Beth's theorem using Craig's lemma.

---

For a different approach, see :

• William Craig, Logic in algebraic form : Three languages and theories (1974), page 44.

See :

• René Cori & Daniel Lascar, Mathematical Logic : A course with exercises. Part I : Propositional Calculus, Boolean Algebras, Predicate Calculus, Completeness Theorems (English ed.2000; French ed.1993), page 42 :

for a proof of the Interpolation lemma and its use in the proof of the Definability theorem for propositional calculus.

For a more "easy" discussion of the issues regarding the treatment of defined symbols in first-order logic, see :

• George Tourlakis, Lectures in Logic and Set Theory. Volume 1 : Mathematical Logic (2003), Ch.I.7. : Defined Symbols, page 112-on

---

---

For a detailed discussion of the fact that

Though deceptively simple and plausible on the face of it, Craig’s interpolation theorem has proved to be a central logical property that has been used to reveal a deep harmony between the syntax and semantics of first order logic.

see :

• Solomon Feferman, Harmonious Logic : Craig’s Interpolation Theorem and its Descendants (2007)