I believe that the answer to your question lies with the Lindenbaum algebra, which is a Boolean algebra (and topological space) that is naturally associated with any formal language, and which provides a way to think about the information content of an assertion. Viewed in this way, the information content of an assertion is not a real number, but rather, is an element of a Boolean algebra, the Lindenbaum algebra. More generally, the information content of a set of assertions is a filter in this algebra.
Namely, consider the set L of all assertions in the language. And consider any theory T in this language. (By the way, your use of the term "universe" in this context is highly nonstandard; a universe is almost universally taken to be a semantic notion, refering to a model or structure satisfying some assertions; what you have in contrast is a syntactic concept, a theory, which is a collection of assertions.)
We may naturally define an equivalence relation on assertions, relative to base the theory T, where φ ≡ ψ if T proves that φ and ψ are equivalent. The collection of equivalence classes forms a Boolean algebra, where [φ] ∧ [ψ] = [φ ∧ ψ] and ¬[φ] = [¬φ]. In particular, there is also the order that comes with any Boolean algebra, which amounts to φ <= ψ just in case T proves that ψ implies φ.
For each assertion ψ, let Fψ be the set of all such consequences of ψ over the theory T. This is, of course, the true "information content" of ψ relative to T. This is a (principal) filter in the Lindenbaum algebra.
More generally,
If S is a theory extending T, then the elements in the Lindenbaum algebra over T corresponding to theorems of S form a filter.
In this case, the Lindenbaum algebra of S is the quotient of the algebra of T modulo this filter.
If S is a complete theory, then the filter is an ultrafilter.
The Stone space (which is compact, Hausdorff, totally disconnected, with a clopen basis) is the set of all ultrafilters, and we may associate any filter (and hence any statement φ) with the collection of all ultrafilters that contain it.
Going back to your question. If I have a collection of axioms A, then I may consider the filter FA that they generate in the Lindenbaum algebra of T. This filter is exactly the same as the set of equivalence classes of consequences of A over T, and is arguably the exact information content of A over T.
For any set of axioms A, the information content FA is precisely the union
Fφ1 ∧ ... ∧ φn, where each φi is in A. But equivalently, we could have said: where each φi is a theorem of A. And because of this, any collection of axioms leading to the same set of theorems will have exactly the same information content, in the sense that the filter that is generated will be exactly the same.
In particular, you use an operation + for adding "information content", and in this context, since we are using filters F to measure information, we naturally define F + G to be he filter generated by F and G together. In this case, I have explained that any choice of axioms leading to the same theorems will have exactly the same sum of information content. Thus, I suppose it is correct to say that they all also minimize that sum as well.
You can read more about the Lindenbaum algebra in Logic, induction and sets, by Thomas Forster. Also, there are many connections to the concept of type theory.
I just noticed the part at the end of your question, about redundancy in axioms. For this, I believe the Lindenbaum algebra is also the right way to think. If you have a list of axioms φ0, φ1, ..., then you can easily remove any redundancy at all by replacing each statement φn with the statement ψn, which asserts: "either φn, or some earlier φi fails". If one removes the logical validities from the new list of axioms, then it is an exercise that none of them implies another, and indeed, no collection of the new axioms implies anything outside that collection. These operations are the Boolean algebraic analogue of "disjointifying" that sometimes occcurs when taking unions of overlapping sets.
