What Formal Mathematics can be Borrowed

Propositions (Inference-free)

This is the least intimate form of borrowing. Essentially what one borrows is whole statements of theorems. The "inference-free" qualifier is meant to distinguish those forms of Proposition (assertoric content) that "precede" formal inference system design, as opposed to those forms, such as sequents, designed as aspects of formal systems. (Presumably these latter forms supplement or elaborate those antecedent forms in order to facilitate argument pertinent to them.)

The most natural sort of propositional borrowing would be simply to take proved propositions (or their translations) from the donor system as true in the recipient system. This is pretty straightforward when the donor and recipient have the same logic or are logics of different kinds but justified by commensurable semantics of propositions.

Inferences and inference-system-specific propositional forms

It may be possible to borrow the more logic-specific inference-laden forms of proposition, such as sequents. Of course, it is also possible that two logics attach distinct semantics to these kinds of propositions, and they might require translation or even be incommensurable.

If one can borrow the inference-system-specific forms of Proposition, one may also be able to borrow Inference Steps, consisting of conclusion/premise complexes of these propositions. Or one may not, since there may be some insurmountable distinction about the semantics of these inferences with premises, since the meaning of an inference with premises may require a special relation between the conclusion and premises beyond the mere fact of logical consequence. (For example, the inference may involve "metavariables" whose semantics involves instantiation across premises and conclusions.)

If one can borrow inferences then one can borrow whole Proofs or derivations as inference trees (or dags).

Justifications of inferences

Even if two systems may accept each others inferences, they might be unable to make sense of the "justificatory" data supplementing inferences which help make them them recognizable as instances of a kind. Significant sharing of Tactic code, for example, can be expected to be quite rare among systems not arising from the same origin. A more likely sharable form of justification would be instances of low-level inference rules that can be independently interpreted by other systems. Thus a donor tactic system ought to be able to provide the "primitive proofs" instead of its tactic code on demand for justifications.

Of course, even if the justificatory data are not literally meaningful to the recipient system, they may yet serve as heuristic data for the method of formal appropriation described in Forms of Sharing Math labeled (4).

Can definitions be borrowed?

Certainly among systems with the same conception of Definition, sharing might be tractable, but it might be less likely than one supposes. The characteristic features of a(n eliminable) symbolic definition are that (1) it stipulates how some syntactic element can be eliminated from expressions (within the definition's "scope") without change of "denotation" of those expressions, and (2) the definition does not count as an extension of the epistemic basis for claims whose meanings depend on that definition. To use such a definition requires only that one understands it as such, and does not require persuading oneself of the meaningfulness or truth of a new primitive; it has more the derived character of a theorem than the primitive character of an axiom.

It is possible that two logics' notion of definition disagree enough on some aspects that some problematic definitions, rather than being translated into definitions in the recipient logic, would have to be employed as part of a translation from the donor to eliminate the defined syntactic elements from propositions. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html