# Are there infinite sets of axioms?

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.

-
Might be a useful post <math.stackexchange.com/questions/309147/…; –  MITjanitor Mar 11 '13 at 5:53
Due to the presence of axiom schemata, $\sf ZFC$ has an infinite number of axioms. However, more can be said, namely, that it is not finitely axiomatizable. This means that it is impossible to replace the infinitely many axioms of $\sf ZFC$ by a finite list. –  Haskell Curry Mar 11 '13 at 10:39
@HaskellCurry Propositional calculus can get founded with axioms and a rule of substitution. Even in that system though we can always get more axioms if we have countably infinite variables. –  Doug Spoonwood Oct 17 '14 at 0:29

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

-

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.

-
Specifically, in Peano, mathematical induction really describes and infinite set of axioms. –  Thomas Andrews Mar 11 '13 at 5:54
I remember of this answer I thought that there's an axiom for every number, but I'm not sure. –  Vÿska Mar 11 '13 at 5:55
I don't think that's true, @GustavoBandeira. –  Thomas Andrews Mar 11 '13 at 6:02
Among the commonly encountered, there are also the theories of vector spaces over a given (infinite) field, of fields of characteristic zero... –  tomasz Mar 11 '13 at 6:18
More interestingly, $\sf ZFC$ is not finitely axiomatizable, as first demonstrated by Richard Montague using the Reflection Principle. –  Haskell Curry Mar 11 '13 at 10:35

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:

• $0 \neq S(0)$;
• $S(0) \neq S(S(0))$;
• $S(S(0)) \neq S(S(S(0)))$;
$\vdots$
• $S ( S ( S ( \cdots ( 0 ) \cdots ) ) ) \neq S ( S ( \cdots ( 0 ) \cdots ) )$
$\vdots$

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

-

Perhaps surprisingly even the classical (Łukasiewicz's) axiomatization of propositional logic has an infinite number of axioms. The axioms are all substitution instances of

• $(p \to (q \to p))$
• $((p \to (q \to r)) \to ((p \to q) \to (p \to r)))$
• $((\neg p \to \neg q) \to (q \to p))$

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.

-
Your semi-decidable set of axioms, however, proves the same theorems as the decidable one where the axioms are those $$\underbrace{x=x\land \cdots\land x=x}_{n\text{ conjuncts}}\land T(m)$$ where $m$ is the representation of a program that terminates in $n$ steps. (Every semi-dedicable set of axioms is equivalent to a decidable one in essentially this way). –  Henning Makholm Mar 12 '13 at 21:58
You can have a recursively enumerable axiom set - it just requires all proofs to include the amount of time before enumerating the axiom. The above is recursively enumerable, so we can prove things in it. The axiom system $S(\pi)$ meaning that $\pi$ does not terminate is not recursively enumerable, and therefore we can't write checkable proofs in that theory. –  Thomas Andrews Aug 11 '13 at 18:07
Lukasiewicz's axiomitization didn't actually use axiom schema. It had 3 axioms and the rule of uniform substitution, which consists of a rule of inference. So actually, the system you've referenced only has 3 axioms. However, even with each axiom as finite, the possible axiomizations of classical propositional logic are infinite since (p→(q→p)) can get replaced by any theorem of the system {(p→(q→p))} under condensed detachment, and since {(p→(q→p))} under condensed detachment has an infinity of theorems. For example, (p→(q→p)) could get replaced by (a→(b→(c→(d→(p→(q→p))))). –  Doug Spoonwood May 7 '14 at 2:19

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:

• Every element of $\mathbb{R}$
• Every element of $\mathcal{P}(\mathbb{R})$
• Every element of $\mathcal{P}(\mathcal{P}(\mathbb{R}))$
• :

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.

-

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.

-
Someone did mention this in another answer. ;-) (BTW: I just pre-ordered a coy of your Introduction to Gödel's Theorems text earlier today. Looking forward to thumbing through it!) –  Arthur Fischer Mar 11 '13 at 9:25
Ooops, sorry @ArthurFischer: very careless reading by me. Enjoy Gödel! –  Peter Smith Mar 11 '13 at 14:21

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.

-