 Both \(\mathbf{IPC}\) and \(\mathbf{IQC}\) satisfy interpolation theorems, e.g.: If \(A\) and \(B\) are propositional formulas having at least one proposition letter in common, and if \(A \rightarrow B\) is provable in \(\mathbf{IPC},\) then there is a formula \(C,\) containing only proposition letters which occur in both \(A\) and \(B,\) such that both \(A \rightarrow C\) and \(C \rightarrow B\) are provable. These topics are treated in Kleene [1952] and Troelstra and Schwichtenberg [2000].