Finite axiomatization of first order logic theories

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!

• The axioms of a first order theory are, in general, intended to be the stuff you add beyond the axioms of pure logic. – Malice Vidrine Aug 30 '18 at 18:30
• It regards the non-logical axioms of the theory. Compare Peano first-order arithmetic with the Induction axiom schema, with its "fragment" : Robinson arithmetic. – Mauro ALLEGRANZA Aug 30 '18 at 18:52

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

• Thank you for your answer! Can you please comment a little bit on how one in practice "quantifies over infinitely many axioms"? I have no intuition about how one in principle would check infinitely many axioms. Please note that my background in logic is elementary. – Daniels Krimans Sep 4 '18 at 16:34
• When a typical theory like Peano arithmetic (PA) has an infinite set of axioms, the infinite part consists of one or more lists of axioms of the same form. For example, the induction axiom scheme in PA has one axiom for each formula $\phi$ of PA, and then each induction axiom looks like $(\phi(0) \land (\forall m)[\phi(n) \to \phi(n+1)]) \to (\forall m) \phi(m)$. So we can list all these in an effective way, and we can tell if an arbitrary statement is one of these axioms. – Carl Mummert Sep 5 '18 at 8:35

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

• Not OP but what theories do you have in mind whose natural axiomatization is infinite but they're finitely axiomatizable? – Alessandro Codenotti Aug 31 '18 at 20:42
• @AlessandroCodenotti ACA$_0$ (= a weak theory for second-order arithmetic - which, despite that term, is in first-order logic - which is extremely important in reverse mathematics and corresponds roughly to the Turing jump) and NF (= an alternate set theory with a number of odd properties), for example. By contrast, neither PA nor ZFC are finitely axiomatizable. – Noah Schweber Aug 31 '18 at 20:43
• @AlessandroCodenotti No; as I said, the phrase "second-order arithmetic" is misleading. The "second-order" there refers to the fact that the theory is intended to describe natural numbers and sets of natural numbers - as opposed to PA, which is only about natural numbers - but it is a first-order theory; just like how ZFC is a first-order theory, despite being about sets. – Noah Schweber Aug 31 '18 at 20:46
• I wrote my (now deleted) comment in between your original one and the edit so I missed the second order bit, makes sense now that you elaborated on it though! Thanks – Alessandro Codenotti Aug 31 '18 at 20:54
• @DanielsKrimans In general there are many ways to axiomatize a given theory. E.g. the theory consisting of all deductive consequences of "$A$" can be axiomatized by $\{A\}$, or by $\{A\wedge A\}$, or by $\{A\vee A, A\rightarrow A, A\wedge A\}$, or by ... You should think of an axiomatization of a theory as a way of producing that theory; in general, the same theory could be produced in different ways. – Noah Schweber Sep 4 '18 at 17:20