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.