Finite axiomatization of first order logic theories

Question

I recently have read that there are set theories (for example, NBG) which are based on the first-order logic and also are finitely axiomatizable.

I am trying to understand what "finitely axiomatizable" means. At first, I thought that it means that it is possible to write all of the axioms as a finite list. In a sense, no axiom schemata occur in the theory.

Then, after consulting book by Kleene "Introduction to Metamathematics" section 19 pages 80-81 where he writes that in propositional calculus $B \implies A \lor B$ is an axiom schema because for every metamathematical expressions $A$ and $B$ it constitutes an axiom, I got confused as how can theories based on first order logic can be finitely axiomatizable if the propositional calculus already has axiom schema.

I would appreciate any comments on this topic!

Answer 1

There are specific deduction systems that have only a finite number of logical axioms, or even no logical axioms. One example is natural deduction, which trades away logical axioms for a more complicated set of inference rules.

However, the use of infinite axiom schemes of logical axioms is not a problem for many of the applications of finite axiomatizability. If we have a structure $M$, or are constructing it, and we want to tell whether $M$ satisfies a theory $T$, there are two main issues we face:

• For each non-logical axiom of $T$, how do we tell that $M$ satisfies the axiom?
• If $T$ has infinitely many axioms, we have to quantify over them somehow.

For finitely axiomatizable theories, the second question is not an issue, so we can focus just on the first one. In any case, we don't need to worry whether our structure $M$ satisfies the logical axioms - we know it does, because they are true in every structure. We only need to worry about whether the structure satisfies the additional axioms of $T$. This is why finite axiomatizability is defined in terms of the non-logical axioms only.

If there are only finitely many new axioms in $T$, we can put all these axioms into a single sentence $\phi$ so that an arbitrary structure satisfies $T$ if and only if it satisfies $\phi$. That is a nice situation to be in, and it allows us in some cases to prove more about finitely axiomatizable theories than we would be able to prove about non-finitely-axiomatizable ones.

The existence of the single sentence $\phi$ also means there is a sort of "absoluteness" to whether a model satisfies $T$. If $T$ has an infinite axiom scheme, then from the point of view of a nonstandard model of arithmetic the scheme may well have nonstandard axioms - this is a subtle issue that can cause various kinds of confusion when people work with Gödel's incompleteness theorem. For a finitely axiomatized theory, because we can work with the single sentence $\phi$, even nonstandard models of arithmetic agree about the axioms for $T$.

Answer 2

Finite axiomatizability (and similar concepts, like recursive axiomatizability) are referring to what is needed beyond the usual logical rules. In particular, a theory $T$ is finitely axiomatizable if there is some finite set $A$ of sentences such that every sentence in $T$ is provable from $A$ using the logical rules/axioms.

Note that axiomatizable is different from axiomatized: it's possible that the "obvious" axiomatization of $T$ is infinite, but there's a clever alternate axiomatization which is finite. There are in fact natural examples of this (if you're interested I can say a bit about these).