Axiom systems and Information Theory Is there a concept of "information" with respect to the axioms of a mathematical system?  
Suppose we have a universe U of theorems.  Suppose an axiom system A=(a1,a2,...) has the universe U as the theorems provable by A.  From an information theory point of view the information in A relative to U = 1.  Denote this as I(A,U) = 1.  Then among all axiom systems with the universe of theorems U, can we find the axiom system B that minimizes I(b1,U)+I(b2,U)+I(b3,U)..., where I(b,U) is the information of b relative to U.
It seems like that among all axiom systems with theorem universe U, B is the axiom system with the minimum redundant information in the axioms of the system.
 A: As stated, I do not believe that the answer has a reasonable answer.  Take as an example the theory of groups, which has both an axiomatization with 1 axiom, and another with 3 (4 if you count closure).  Is the 1-axiom version really `better', even from an information-theoretic point-of-view?  You need to actually ask which encoding of these 2 (in some system) is shortest - and for all intents and purposes, the 3-axiom version will be shorter.
For the case where you have an infinite number of axioms, things get more complicated, as you need to make sure you still have a proper information measure (i.e. of total weight $\leq 1$), which is not always easy to achieve in a natural manner.  
On the other hand, suitably rephrased, I do believe your general question has a positive answer.  Just don't expect there to be a unique minimal system, in the same way one cannot hope to define the 'unique' simplification of an expression (Google for "understanding expression simplification" if you want details).
A: 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.
A: C.S. Peirce proposed a logical framework for information theory as far back as 1865, suggesting that the "laws of information" were key to unlocking the puzzle of how scientific inquiry works.  He later formulated a logarithmic measure for information content and pursued his ideas about information in parallel with his attempts to articulate modal logics in the diagrammatic syntax of logical graphs.
You may find it worth your while to look into some of this work.  The following web page contains a very rough set of notes that will serve to provide further links:
Information = Comprehension × Extension
