Rosetta stone in the book "New Structures in Physics" (http://www.springer.com/la/book/9783642128202) is the correspondence between the propositional (linear) logic from the one side and the monoidal categories from the other side. Each proposition can be represented as the object, each deduction (proof) among two literals can be represented as the morphism between repsective objects and each connective can be attributed to the tensor product among objects in category. That works for propositional logic.
The similar correspondence can be extended to the modal logics and modal operators, e.g. in paper http://www.cs.nott.ac.uk/~psznza/papers/Alechina++:01a.pdf
The question is: can this correspondence between logic (deductive system) and the category theory be extended to the predicate logic? There is article where it has been done (it is said so) http://amcm.pcz.pl/get.php?article=2015_1/art_03.pdf This extension is done in chapter 4 of this article. The problem is - I don't understand this chapter from the very basic things. The authors say that predicate can be expresses by the subset of the object - but there is no such notion in the category theory. Maybe someone can explain chapter 4 or give alternative correspondence between predicate logic and category theory?
This correspondence is very exciting subject because it can lead to the universal logic and universal reasoning system - very much welcome in the applied AI!
So there seem to be a couple of questions you are asking, though the answer is "yes" to both of them.
You mention linear logic, but a lot of your questions are not restricted to linear logic, maybe because you intended that to be implied. Either way, I'll talk about (non-linear) predicate logic and the linear case.
As far as extending categorical semantics beyond propositional logic, the answer is a resounding "yes". Essentially all forms of logic and type theory have been given categorical semantics, or failing that, the expectation is that you can give them categorical semantics. Roughly speaking, a category gives rise to a logic/type theory and vice versa so there is always a "categorical semantics". The work is mostly one of giving reasonable presentations on each side and connecting examples. At this point, there's an interplay between logic/type theory and category theory. For example, the very recent Homotopy Type Theory arose due to Voevodsky starting to play with Coq. He wondered what the semantics were and realized that they formed an internal language for $\infty$-groupoids an area categorists had been studying furiously around that time.
For study, I liked Andrew Pitts' notes on Categorical Logic though they are a bit dated now. Bart Jacobs' thesis or book is very comprehensive though not the most accessible thing.
For linear logic, most of the study has been on the propositional fragment. (This monograph, Categorical Semantics of Linear Logic, looks like it is a fairly comprehensive introduction to that work, but, as mentioned, doesn't cover quantification in linear logic.) As a type theory this corresponds to a simply typed linear lambda calculus. The corresponding language for linear predicate logic would be dependent linear type theory. This is a relatively young area of research from both the category theory side and the type theory side. The page just referenced includes links to further references, one of which, which most directly addresses your question, is Syntax and Semantics of Linear Dependent Types. Skimming it, it doesn't look like it would be very approachable for someone relatively new to categorical logic/type theory. Roughly, the current situation is categorical semantics for dependent type theory is well understood and categorical semantics for linear logic is well understood, and we're in the process of combining those two sizeable areas of study into categorical semantics of linear dependent type theory.