The Form of the Problem
The form of the problem we consider is how to produce a candidate for a proof in a "recipient" system that borrows results from a "donor" system, and how one would argue for the result's correctness in the recipient's logic. We use "logic" in a sense that two systems can share a common logic but with some different primitives, including axioms. A logic in this sense characterizes not a specific class of theorems or inferences but rather proof structure. When multiple systems serve as mutual donors we would have a hybrid system proper.
We approach the problem from two directions: the