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.

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.
