I'm reading Behnke's Fundamentals of mathematics:
If the number of axioms is finite, we can reduce the concept of a consequence to that of a tautology.
I got curious on this: Are there infinite sets of axioms? The only thing I could think about is the possible existence of unknown axioms and perhaps some belief that this number of axioms is infinite.
On
Many important theories, most significantly first-order Peano arithmetic, and ZFC, the most commonly used axiomatic set theory, have an infinite number of axioms. So does the theory of algebraically closed fields.
On
Are there infinite sets of axioms? Yes!
As a trivial (and somewhat meaningless) example, consider the first-order language whose only non-logical symbols are the constant symbol $0$ and the unary function symbol $S$. Then the following would comprise an infinite set of axioms:
For a more meaningful example we have, as others have pointed out, Peano Arithmetic. More than just being an infinite list of axioms, this theory necessarily has an infinite set of axioms. By a result of C. Ryll-Nardzewski, (assuming it is consistent) Peano Arithmetic is not finitely axiomatisable: there is no finite set of axioms (in the same language) that has the same collection of formal theorems. (A similar result holds for ZF(C).)
On
As others have noted, first order PA has an infinite number of axioms. But it is worth stressing that this is not just a superficial feature of the usual mode of presenting the induction axioms via a schema or template. It is provable that there is no finitely axiomatized theory in the language of PA whose theorems coincide with those of PA.
On
Perhaps surprisingly even the classical (Łukasiewicz's) axiomatization of propositional logic has an infinite number of axioms. The axioms are all substitution instances of
so we have an infinite number of axioms.
Usually the important thing is not if the set of axioms is finite or infinite, but if it is decidable. We can only verify proofs in theories with decidable sets of axioms. If a set of axioms is undecidable, we can't verify a proof, because we can't tell if a formula appearing in it is an axiom or not. (If a set of axioms is only semi-decidable, we're able to verify correct proofs, but we're not able to refute incorrect ones.)
For example, if I construct a theory with the set of axioms given as
$T(\pi)$ is an axiom if $\pi$ is a representation of a terminating program.
Then I can "prove" that some program $p$ is terminating in a one-line proof by simply stating $T(p)$. But of course such theory has no real use because nobody can verify such a proof.
On
An example of an infinite set of axioms used for practical use is the foundation of non-standard analysis.
Create a first-order language whose symbols include:
Now select a set of axioms to be the set of all true statements in this language.
This language and set of axioms is enough to do lots of things; e.g. any theorem you've learned in calculus can be stated in this language and is automatically a theorem.
By general properties of first-order logic, this set of axioms is consistent and thus there exists a non-standard model! By construction, every theorem you know about 'standard' things is automatically true for non-standard things as well! In this formulation, the transfer principle from non-standard analysis -- every 'standard' object has a nonstandard analog, and every statement of 'standard' analysis is true if and only if its translation to the non-standard model is true -- becomes an utter triviality.
While one can surely attempt to select a smaller set of axioms, there is no actual reason to; for the specific application we have to apply logic in this instance, it is by far easier and more convenient to take all of them.
On
Just to make the matter maybe a bit more clear giving another example:
Similar to what André Nicolas stated, $ACF_0$ (the theory of algebraically closed fields of charateristic $0$) is axiomatized by $ACF$(the theory of algebraically closed fields) + $\{\neg\phi_p$ : $p$ is prime$\}$, where $\phi_p$ says "I have characteristic $p$." $ACF$ is already not finitely axiomatizable itself but I am sure observing that $\{\neg\phi_p$ : $p$ is prime$\}$ is an infinite set of axioms is way more obvious.
In first order Peano axioms the principal of mathematical induction is not one axiom, but a "template" called an axiom scheme. For every possible expression (or "predicate") with a free variable, $P(n)$, we have the axiom:
$$(P(0) \land \left(\forall n: P(n)\implies P(n+1)\right))\implies \\\forall n: P(n)$$
So, if $P(x)$ is the predicate, $x\cdot 0 = 1$ then we'd have the messy axiom:
$$(0\cdot 0=1 \land \left(\forall n: n\cdot 0 =1\implies (n+1)\cdot 0=1\right))\implies \\\forall n: n\cdot 0 = 1$$
Our inclination is to think of this axiom scheme as a single axiom when preceded by "$\forall P$", but in first-order theory, there is only one "type." In first-order number theory, that type is "natural number." So there is no room in the language for the concept of $\forall P$. In second order theory, we can say $\forall P$.
In set theory, you have a similar rule, the "axiom of specification" which lets you construct a set from any predicate, $P(x,y)$, with two free variables:
$$\forall S:\exists T: \forall x: (x\in T\iff (x\in S\land P(x,S)))$$
(The axiom lets you do more, but this is a simple case.)
which essentially means that there exists a set:
$$\{x\in S: P(x,S)\}$$
Again, there is no such object inside set theory as a "predicate."
For most human axiom systems, even when the axioms are infinite, we have a level of verifiability. We usually desire an ability to verify a proof using mechanistic means, and therefore, given any step in a proof, we desire the ability to verify the step in a finite amount of time.