Is Kripke Platek theory finitely axiomatizable?

Question

I know that closure under the Gödel operations is equivalent to $\Delta_0$-separation (plus extensionality, union, pair, foundation). This is finitely axiomatizable. But when we add $\Delta_0$-collection, to obtain KP, is it still finitely axiomatizable? And in this case, how to prove it?

Answer 1

The answer to the question depends on how "foundation" is formulated, i.e., as a single axiom or as a full scheme (one which makes sure that every nonempty parametrically definable class has a minimal element, equivalently: the principle of $\in$-induction holds). Emil Jeřábek 's answer pertains to the latter formulation, but not the former.

In the old days, beginning with Barwise, KP was defined so as to include the full scheme of foundation, perhaps because of the fact that KP was designed to study the class of well-founded models of a well-behaved fragment of ZF. But this has changed somewhat, for example in Adrian Mathias' paper The Strength of MacLane Set Theory (Annals of Pure and Applied Logic, 2001) KP only includes $\Pi_1$-Foundation, asserting that every nonempty $\Pi_1$-definable class (parameters allowed) has a minimal element (see p.111 of the above hyperlinked text).

It is well-known that KP as defined by Mathias is finitely axiomatizable. The proof uses the fact that there is a definable truth definition for $\Pi_1$-formulae in KP.

Answer 2

As I’ve already explained in more detail in https://mathoverflow.net/a/87249, every sequential theory whose interpretation of arithmetic satisfies the induction schema for all formulas in the language of the theory is uniformly essentially reflexive, and consequently, not finitely axiomatizable (unless inconsistent). The Kripke–Platek set theory is indeed a sequential theory with full induction: specifically, induction over $\omega$ follows from the axiom schema of $\in$-induction.

So, KP is not finitely axiomatizable, and the culprit is foundation ($\in$-induction); collection is largely irrelevant for the result. Note that in ZF, $\in$-induction is equivalent to a single axiom, but the full schema of separation is needed to prove that. In its absence, the foundation schema of KP is not finitely axiomatizable.