| 1. | direct incorporation of results when the donor logic is also the recipient logic (modulo name collision and accounting for base differences such as axioms) |
| 2. | informal inference from one system to another -- Here one selects entities of one system, or translations of them, and takes them as new primitives in the recipient system, their occurrences in the old system standing as mere informal justification of their plausible adoption. This uses the same mechanism as simply stipulating new primitives, indicating informal reasons as part of the stipulation. This is the special case of making some informal appeal to another independent formal development (it could prevent cycles of such informal justification, though). |
| 3. | direct or translated formal inference across systems (perhaps some offerings are rejected by the recipient) |
| 4. | formal appropriation -- Rather than selecting entities to be accepted informally, one directly justifies them or their translations, using the donor's proof not as evidence but as advice on how to establish the results by the recipient's own methods. |
Discussion of Basic Forms of Borrowing
We presuppose adequate accounting methods for possible differences in logical bases such as axioms and logics. Forms (1) and (2) are both simpler conceptions than the others, and we take them as more basic.
Forms (1), (2) and (4) are logically light-weight methods, whereas (3) can require substantial semantic or proof theoretic work.
Forms (1), (3) and (4) are all directed at extending the formal methods formally, systematically preserving validity of results in the recipient logic. One argues generally that the result is correct based upon the correctness of the recipient logic and the method for borrowing (which in (3) requires argument for correctness of the donor logic).
Form (2) on the other hand, is an ad hoc extension which essentially amounts to adopting new primitives. The cross system dependency is purely informal, but explicit. The argument for validity depends upon informal argument for the acceptance of new primitives, the references to the donor sources serving merely as elements of informal arguments for plausibility.
Form (1) is the most obvious method, amounting to accounting for different primitives that the donor and recipient might use, but otherwise introducing no significant commitment to theory or computation beyond the logic. Note that there is no automatic guarantee that combining primitives is consistent, hence the need for accounting.
Forms (3) and (4) can both be seen as methods for rehabilitating method (2) to eliminate the ad hoc arguments for plausibility of the borrowed entities. Form (3) is likely to be theoretically heavy but computationally light; (4) is likely to be computationally heavy but theoretically light.
While (3) produces proofs in the recipient system whose justification is based upon the logic (semantics or proof theory) of the donor system, (2) and (4) are not deductively based upon the donor logic at all, but simply treat the occurrences in the donor logic as plausible suggestions, which in the method of (4) are filtered automatically down to valid borrowings, and in (2) are filtered provisionally admitting possibly invalid borrowings.
Forms (3) and (4) may give rise to what might be considered hybrid "proof systems", the former comprising a hybrid "logic" and the latter a hybrid "system" for combining proofs without any inter-logic negotiations.
These considerations lead us to consider