Category theorists stance on deductive systems

This sentence reads to me like "we will treat Xs as if they were special kinds of of Ys, which will make both X-theorists and Y-theorists unhappy because it is not true". Reminds me of the old joke when a patient says "Doctor, it hurts when I do this" and the doctor says "Then don't do that!"

I think a more modern thing to say is that a deductive system describes a sort of algebraic theory, where the axioms and rules of inference are the operations. The inductively defined derivable judgments are the elements of the initial/free algebra for this algebraic theory; whereas there are of course also algebras that are not free. In particular, the deductive system is a theory that is not identified with any of its algebras, either the free ones or the non-free ones. Computer scientists may be most interested in the free algebras, whereas category theorists are interested in all the algebras (although of course the free ones play an important role).

I think the idea should pretty much like this: once you drop the requirement for the deductive system to be freely generated from the axioms by the inference rules (i.e. you accept the existence of non free deductive systems) you can start to study morphisms from the free deductive systems into not free ones (what Lambek and Scott call functors, if memory serves me well).

In this way you can hopefully prove properties of the free systems by looking to the not free ones. For instance for proving that two proofs (i.e. arrows) are different in a free deductive system you could try to find a nice functor that sends the said proofs in different arrows. Here by nice I mean that such functor sends the proofs in a different system where it is easier to prove the inequality of the two proofs.

As a example (probably a not really interesting one) you can consider the functor that goes from a syntactic-freely generated deductive system to the deductive system $\mathbb N$ (the additive monoid of natural numbers, seen as a category, hence as a deductive system), that sends every object (proposition) to the only object of the one-object category $\mathbb N$ and every morphism/proof to its length (which is indeed a natural number, that is a morphism in $\mathbb N$). This functor allows one to distinguish between two proofs because they have different length.

I suppose that someone with much more knowledge on the subject than me can provide some more interesting examples.