Der Interpolationssatz der intuitionistischen Prädikatenlogik (Q1130509)

The author gives a beautifully elegant proof of the interpolation lemma and the definability theorem for intuitionistic predicate logic, first established by \textit{W. Craig} [J. Symb. Log. 22, 269--285 (1957; Zbl 0079.24502)] and \textit{E. W. Beth} [Nederl. Akad. Wet., Proc., Ser. A 56, 330--339 (1953; Zbl 0053.34402)] respectively for classical logic. The proof uses the author's cut free formalisation of intuitionistic predicate logic [Math. Ann. 122, 47--65 (1950; Zbl 0036.14801)]. As he points out, the proof extends to the minimal calculus (i. e. intuitionistic logic without negation). The author's paper supersedes the reviewer's abstract [``Explicit definability in intuitionistic logic''. J. Symb. Logic 25, 389--390 (1960)] where some trivial special cases were established. As was pointed out in the abstract, (i) the interpolation lemma for the classical calculus is an immediate consequence of the author's result, but not conversely: algebraically speaking the interpolation lemma is a lattice theoretic fact and not specially concerned with boolean structures; (ii) because of the independence of the logical constants \(\neg, \wedge, \vee, \rightarrow, \bigwedge ,\bigvee\), in intuitionistic logic it makes sense (in contrast to the classical case) to ask whether, if \(A\rightarrow B\), there exists an interpolation formula \(C\) (i. e. \(A\rightarrow C\) and \(C\rightarrow B\), \(C\) containing only non-logical constants common to \(A\) and \(B\)) such that \(C\) contains as logical constants only those common to \(A\) and \(B\). The author notes some partial results on this. Finally, it should be observed that from a given derivation of \(A\rightarrow B\), an interpolation formula \(C\) is obtained in a purely finitist (even primitive recursive) manner. It is known that this result has to refer explicitly to an hypothetical derivation since there exists no recursive function \(\varphi(A, B)\) whose value is an interpolation formula \(C\) with the property: if \(\vdash A\rightarrow B\), then \(\vdash A\rightarrow \varphi(A, B)\) and \(\varphi(A, B)\rightarrow B\), as shown in [Techn. Rep. No. 3, Da-04-200-ORD-997, Appl. Math. Stat. Lab., Stanford 1961, 3, 37--38].