What is the reason for having a minimal set of axioms in first-order logic?

Question

Another way of getting at the same thing : from the standpoint of mathematical logic, does it cause any difficulties to add theorems of first-order logic as axioms?

Answer 1

In formalizing a theory, there is always a trade-off between economy-of-apparatus and practicality-of-use.

Take, for example, the standard textbook Hilbert-style of axiomatisation of propositional logic using just $\to$ and $\neg$, with three axiom schemas plus modus ponens.

A beautifully simple theory, but a real pain to actually use if we insist that every proof is done from first principles, and can't invoke previously-proved theorems without proving them again.

Does having a rule that allows us to recycle previously proved propositions count as "adding theorems as axioms"? Well, no, we certainly aren't changing what counts as an official axiom of the logic. Well, yes, we are changing what we can appeal to in a proof: we have new propositions which we treat on a par with axioms as not themselves needing justification within the proof.

If we want to use a theory to prove things, having a rule that allows us to invoke established theorems as in effect additional axioms is pretty essential to ease-of-use. If we want to theorise about a theory, the unadorned original theory gives us something neater to do our metatheory about.