Strong Paraconsistency by Separating Composition and Decomposition in Classical Logic

In this paper I elaborate a proof system that is able to prove all classical first order logic consequences of consistent premise sets, without proving trivial consequences of inconsistent premises (as in A, (sic)A proves B). Essentially this result is obtained by formally distinguishing consequences that are the result of merely decomposing the premises into their subformulas from consequences that may be the result of also composing 'new', more complex formulas. I require that, whenever 'new' formulas are derived, they are to be preceded by a special +-symbol and these +-preceded formulas are not to be decomposed. By doing this, the proofs are separated into a decomposition phase followed by a composition phase. The proofs are recursive, axiomatizable and, as they do not trivialize inconsistent premise sets, they define a very strong non-transitive paraconsistent logic, for which I also provide an adequate semantics.