Are there any documented logics that use transitivity of implication rather than modus ponens as a primitive? Are there any documented logics that use transitivity of implication rather than modus ponens as a primitive?  The type theoretic equivalent would be a lambda calculus that uses functional composition rather than function application as a primitive.
 A: I presume that by "transitivity" you mean the rule $A \to B \ , \ B \to C \vdash A \to C$ for any sentences $A,B,C$. I don't have references, but just for record here is the general way to completely replace modus ponens in any Hilbert-style system by the transitivity rule plus two additional rules. Any sentence $A$ can be proven in the original system iff it can be proven in the new system. The extra rules are:

Top introduction rule:   $A \vdash \top \to A$   for any sentence $A$.
Top elimination rule:   $\top \to A \vdash A$   for any sentence $A$.

Here "$\top$" is a new propositional symbol that should be interpreted as "anything". This makes sense from computability perspective, and $\top$ can also be taken as the top type.
To prove the claim about the new system, we shall use induction over the length of the proof in the original system, and prove the stronger invariance that for every deduced sentence $Q$ in that proof we can deduce in the new system both $Q$ and $\top \to Q$. If $Q$ is an axiom, then by top introduction we can deduce $\top \to Q$ in the new system. If $Q$ is the result of modus ponens on $P$ and $P \to Q$ for some previously deduced sentence $P$, then by the invariance we can deduce $\top \to P$ in the new system, and hence can deduce $\top \to Q$ by transitivity, and also $Q$ by top elimination.

We can remove the top introduction rule simply by modifying each axiom $A$ to $\top \to A$. The proof is the same as above.

We can also replace the top elimination rule by an axiom:

Top elimination axiom:   $( \top \to A ) \to A$   for any sentence $A$.

But then I think we need another extra rule such as:

Swap rule: $A \to ( B \to C ) \vdash B \to ( A \to C )$ for any sentences $A,B,C$.

And we need to relax the requirement to that any sentence $A$ can be proven in the original system iff $\top \to A$ can be proven in this new system.
The proof is similar. We change the invariance to only require that for every deduced sentence $Q$ in the original proof we can deduce $\top \to Q$ in the new system. This time, if $Q$ is the result of modus ponens on $P$ and $P \to Q$ for some previously deduced sentence $P$, by the invariance we can in the new system deduce $\top \to P$ and $\top \to ( P \to Q )$. If we have the swap rule, then we can deduce $P \to ( \top \to Q )$, and hence $\top \to Q$ by transitivity and the top elimination axiom.
Interestingly, in this last approach the only two rules, namely transitivity and the swap rule, correspond to the well-known combinators for program composition and program input swapping (at least when interpreted in uncurried form).

I believe but cannot quite formalize the intuition that there is no uniformly computable way to convert the original system to an equivalent one that has the transitivity rule and no other rule (even if additional axioms are allowed).
