The related question is:

Is Kripke Platek theory finitely axiomatizable?

My questions are as follows:

Let $\mathsf{KP}$ be the Kripke Platek set theory with only $\Pi_1$-foundation, and *without* the axiom of infinity.

Let $\mathsf{KPI}=\mathsf{KP}+{}$ the axiom of infinity.

On page 165, line 17 of Mathias's paper The strength of Mac Lane set theory, it is claimed that $\mathsf{KPI}$ is finitely axiomatizable, and on page 47 of his handwritten notes Notes on set theory (see T215 there), this fact is proved.

**Is $\mathsf{KP}$ also finitely axiomatizable?**

In fact, I do not even know the following things about $\mathsf{KP}$:

1, Is "$x$ is finite" $\Delta_1^{\mathsf{KP}}$ ?

2, Can $\mathsf{KP}$ prove that "for all finite $x$, the power set of $x$ exists"?

3, Can $\mathsf{KP}$ prove that "if there is an infinite set, then $\omega$ exists"?

4, Can $\mathsf{KP}$ prove that "for all $x$, if $\mathrm{rank}(x)<\omega$, then $x$ is finite"?

5, In $\mathsf{KP}$, do we have the truth definition as in $\mathsf{KPI}$?

where "$x\in\omega$" is defined to be "$x$ and all its members are 0 or successor ordinals", and "$x$ is finite" is defined to be "$\exists n\in\omega\exists f($ $f$ is a bijection from $n$ onto $x$ $)$"; the rank function is defined in $\mathsf{KP}$ by the "definition by recursion" theorem.

My another related question about the finite axiomatizability of $\mathsf{KPI}$ is:

If we extend $\mathsf{KPI}$ to contain also $\Sigma_n$-separation, $\Sigma_n$-collection, and $\Pi_n$-foundation, is this extension still finitely axiomatizable?

Edit: The answer to the question 2 is affirmative, as shown in Proposition 2.13 on page 161 of Mathias's paper *Weak Systems of Gandy, Jensen and Devlin*.