Suppose φ ⊨ ψ, where φ uses predicate symbols {P, Q, R} and ψ uses predicate symbols {Q, R, S}. What can be said about the vocabulary of any interpolant θ?
Aθ must use all symbols from both φ and ψ: {P, Q, R, S}
Bθ's vocabulary must be a subset of {Q, R} — the symbols shared by φ and ψ
Cθ must be logically equivalent to φ, so it uses exactly {P, Q, R}
Dθ may use any symbols since its purpose is to bridge different vocabularies
Craig's theorem guarantees an interpolant whose non-logical vocabulary is contained in the intersection of φ's and ψ's vocabularies — here {Q, R}. The symbols P (unique to φ) and S (unique to ψ) cannot appear in θ. The key insight is that when φ ⊨ ψ, the logical connection between them must be expressible entirely in terms of what they share. P is relevant to φ's internal structure, but whatever role it plays in implying ψ can be captured by a formula using only Q and R.
Question 2 Multiple Choice
Beth's definability theorem states that if a predicate P is implicitly defined by a theory T, then:
AP cannot be eliminated from T without changing which sentences T proves
BP is explicitly definable by a formula in T's vocabulary not containing P
CT must be categorical — having only one model up to isomorphism
DP appears essentially in every axiom of T
Beth's theorem: implicit definability implies explicit definability. If T implicitly defines P (any two models of T agreeing on all non-P symbols must also agree on P's extension), then there is a formula φ(x) in T's P-free vocabulary such that T ⊢ ∀x(P(x) ↔ φ(x)). The proof uses Craig interpolation: implicit definability yields an entailment between two copies of T (one using P, one using renamed P'), and the shared vocabulary is everything except P and P'. The interpolant provides the explicit definition. This is the theorem's non-trivial content — semantic uniqueness forces syntactic expressibility.
Question 3 True / False
For a given entailment φ ⊨ ψ, Craig's theorem guarantees exactly one interpolant — a unique sentence in the shared vocabulary mediating the entailment.
TTrue
FFalse
Answer: False
The interpolant is not unique. Any sentence θ in the shared vocabulary satisfying φ ⊨ θ and θ ⊨ ψ qualifies. You could strengthen or weaken θ within the shared vocabulary and still have a valid interpolant, as long as it remains between φ and ψ in logical strength. Craig's theorem guarantees existence, not uniqueness. In practice, interpolants can vary enormously in complexity and form, which is why constructive interpolation proofs (extracting an interpolant from a proof of φ ⊨ ψ) are valuable — they produce a specific witness, but other witnesses also exist.
Question 4 True / False
Craig's interpolation theorem applies to standard first-order logic but fails for some extensions, such as logics with generalized quantifiers.
TTrue
FFalse
Answer: True
Craig interpolation is a property that first-order logic has and many of its extensions do not. Logics with generalized quantifiers (e.g., 'there exist infinitely many x such that...'), certain fragments of second-order logic, and various modal logics can fail interpolation — meaning there exist entailments φ ⊨ ψ for which no interpolant exists in the shared vocabulary. This failure is significant: it indicates that the entailment cannot be fully decomposed into shared content, revealing a structural difference between these logics and FOL. Interpolation is often treated as a robustness property that makes a logic well-behaved.
Question 5 Short Answer
In your own words, what does Craig's interpolation theorem say about the 'common content' mediating a logical entailment between two sentences?
Think about your answer, then reveal below.
Model answer: If φ logically implies ψ, then the connection between them can be fully expressed using only the vocabulary they share. There is always an intermediate sentence θ — the interpolant — that uses only the shared predicate, function, and constant symbols, such that φ implies θ and θ implies ψ. The symbols unique to φ and unique to ψ play no essential role in the logical relationship between them; the entailment is entirely 'carried' by the shared vocabulary.
This theorem reveals that logical entailment is local to shared content — two sentences cannot be logically connected through vocabulary that only one of them uses. It has practical applications in computer science (modular verification, where you check components share sufficient interface to guarantee a system property) and in philosophy of science (showing that theoretical terms linking two theories must have a common empirical content).