Question: This question was inspired by [this](https://math.stackexchange.com/questions/111428/lemma-vs-theorem) question. 

Does it really make sense to say that a formal system has some number of axioms, say three, or ten, etc? E.g., take a formal system that admits conjuction elimination and has axioms $ A\_1, A\_2,..., A\_n $. But a formal system that has the single axiom $ A\_1\wedge A\_2\wedge ...\wedge A\_n $ is essentially the same formal system!

So, is the concept of number of axioms in a formal system subjective, just as there is no objective difference between a lemma and a theorem?

**P.S.** I'm indeed talking about finitely axiomatizable formal systems only. I.e. when I say "axioms", I mean it - no axiom schemata allowed.

Answer: 
If you step out of boolean logic and look at multivalued logics, there are places where having a conjuction (for example in BL (<http://en.wikipedia.org/wiki/BL_%28logic%29>) if you conjunct the axioms with what is known as strong conjunction) is different from having the axioms separately (i.e. the sets of deductions won't match up properly).

In the boolean case, the number of axioms (I'm talking about finite axiomatizations as asked in the question) doesn't really matter if you are interested in the theorems. But the derivation of a proof (in a formal system) will be different. However there is good reason to split up the axioms and talk about them separately; the human mind just deals with that approach better.
First off, let's make things clear and point out that not all theorems are the same even from a syntactic point of view. Some theorems can serve as a single axiom for some logical system in the sense that under some rule of inference, some theorem can get generated from that axiom which is not a substitution instance of the axiom. Other theorems can't generate anything under that same rule.

For instance, in some systems with detachment as the rule of inference, CCpqCCqrCpr is a theorem. If the system has countably infinite variables, the system {CCpqCCqrCpr} under detachment and substitution has countably infinite theorem which are not substitution instance of CCpqCCqrCpr. On the other hand, in some systems CCCpqpp is a theorem. But, the system {CCCpqpp} only has substitution instance of CCCpqpp as theorems.

Now one part of a formal system, according to [Wikipedia](http://en.wikipedia.org/wiki/Formal_system) consists of its deductive apparatus. The deductive apparatus consists of the axioms and/or rules of inference of the formal system. Thus, if the axioms differ, we have a different deductive apparatus. Consequently, even though the consequences of two deductive apparatuses may end up the same, the deductive apparatuses differ and consequently the formal systems differ. Axioms also differ from theorems in that they belong to the deductive apparatus, while theorems do not (at least according to the Wikipedia definition). Additionally, in terms of proving certain theorems, or what can/has gotten called the development of a formal system, the systems can differ in that some theorem might come as provable in fewer steps in system A than in system B.

So, no, the concept of the number of axioms in a formal system is not subjective. And yes it makes sense to say that a formal system has a certain natural number of axioms.