I have three questions about logic, concretely about Craig's and Lyndon's Interpolation Theorems.
In Boolos et al 'Computability and Logic' there is a very convincing proof of the former which first deals with the case where identity and functions symbols are not present.
The approach must be correct, since if it worked with identity present it would give us a stronger and incorrect version of Craig's Theorem. However, I fail to see how the proof stops working if we repeated the argument with identity present. That's my first doubt.
The second has to do with proving Lyndon's Theorem, which is suggested as an exercise at the end of the chapter.
I tried replicating Craig's proof, but the introduction of identity does not work as expected, since the axioms introduced to eliminate identity introduce both positive and negative occurences of each predicate in the sentences, making it impossible to apply Lyndon's in the case without identity in a meaningful way.
At last, it is said in the book that Lyndon's theorem does not work if constants are present, but I am starting to seriously doubt this. In Lyndon's original paper there is nothing said about that failure (he does not contemplate constants per se, but he contemplates functions, and a constant can be viewed as a $0$-ary function, right?), and I could not find a suitable counterexample.
Any suggestion regarding any of my three doubts?
Proof of Craig's Interpolation Theorem:
The exercises where Lyndon's Theorem appears:
