Is there such a thing as the number of axioms?

Question

This question was inspired by this 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 1

Certainly if I give you a formal system with an explicit list of axioms, say 42 of them, then it makes sense to say that the system has 42 axioms. It's hard to dispute that.

But you make a good observation, that there many equivalent formal systems with all sorts of different numbers of axioms. To be precise, say two formal systems (using the same symbols) are equivalent if they prove exactly the same theorems. It's often useful consider formal systems only up to equivalence, when what we care about is the theorems they prove, not their presentations.

So the question is really about whether by formal system you mean "explicitly defined formal system" or "formal system up to equivalence". The former has a well-defined number of axioms, the latter does not.

Answer 2

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 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.

Answer 3

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.