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.